fix: resolve ofNat vs natCast confusion in a Fin lemma (#17422)

leanprover-community · Oct 7, 2024 · 78b3a02 · 78b3a02
1 parent b53b6c3
commit 78b3a02
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
@@ -1514,10 +1514,16 @@ lemma sub_succ_le_sub_of_le {n : ℕ} {u v : Fin (n + 2)} (h : u < v) : v - (u +
 end AddGroup
 
 @[simp]
-theorem coe_ofNat_eq_mod (m n : ℕ) [NeZero m] :
+theorem coe_natCast_eq_mod (m n : ℕ) [NeZero m] :
     ((n : Fin m) : ℕ) = n % m :=
   rfl
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem coe_ofNat_eq_mod (m n : ℕ) [NeZero m] :
+    ((no_index OfNat.ofNat n : Fin m) : ℕ) = OfNat.ofNat n % m :=
+  rfl
+
 section Mul
 
 /-!

diff --git a/Mathlib/Logic/Equiv/Fin.lean b/Mathlib/Logic/Equiv/Fin.lean
@@ -470,7 +470,7 @@ def Int.divModEquiv (n : ℕ) [NeZero n] : ℤ ≃ ℤ × Fin n where
   toFun a := (a / n, ↑(a.natMod n))
   invFun p := p.1 * n + ↑p.2
   left_inv a := by
-    simp_rw [Fin.coe_ofNat_eq_mod, natCast_mod, natMod,
+    simp_rw [Fin.coe_natCast_eq_mod, natCast_mod, natMod,
       toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
       ediv_add_emod']
   right_inv := fun ⟨q, r, hrn⟩ => by