From 78b3a02235527543f0c61118f06b48d44fa96a32 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 7 Oct 2024 12:39:02 +0000
Subject: [PATCH] fix: resolve ofNat vs natCast confusion in a Fin lemma
 (#17422)

---
 Mathlib/Data/Fin/Basic.lean  | 8 +++++++-
 Mathlib/Logic/Equiv/Fin.lean | 2 +-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
index d875809cf1a4a..e0de8283c150d 100644
--- 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
index 1d07d2d1b2b25..3453d19eac020 100644
--- 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