chore: forward-port leanprover-community/mathlib#18131 (#2178)

* [`data.fin.basic`@`7c523cb78f4153682c2929e3006c863bfef463d0`..`008af8bb14b3ebef7e04ec3b0d63b947dee4d26a`](https://leanprover-community.github.io/mathlib-port-status/file/data/fin/basic?range=7c523cb78f4153682c2929e3006c863bfef463d0..008af8bb14b3ebef7e04ec3b0d63b947dee4d26a)

Mathlib/Data/Fin/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Keeley Hoek
 
 ! This file was ported from Lean 3 source module data.fin.basic
-! leanprover-community/mathlib commit 7c523cb78f4153682c2929e3006c863bfef463d0
+! leanprover-community/mathlib commit 008af8bb14b3ebef7e04ec3b0d63b947dee4d26a
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -2485,16 +2485,10 @@ theorem coe_clamp (n m : ℕ) : (clamp n m : ℕ) = min n m :=
 #align fin.coe_clamp Fin.coe_clamp
 
 @[simp]
-theorem coe_ofNat_eq_mod' (m n : ℕ) [NeZero m] :
-    (@Fin.ofNat' m n (Nat.pos_of_ne_zero (NeZero.ne m)) : ℕ) = n % m :=
+theorem coe_ofNat_eq_mod (m n : ℕ) [NeZero m] :
+    ((n : Fin m) : ℕ) = n % m :=
   rfl
--- Porting note: new in mathlib 4?
--- #align fin.coe_of_nat_eq_mod' Fin.coe_ofNat_eq_mod'
-
-@[simp]
-theorem coe_of_nat_eq_mod (m n : ℕ) : ((n : Fin (m+1)) : ℕ) = n % Nat.succ m :=
-  rfl
-#align fin.coe_of_nat_eq_mod Fin.coe_of_nat_eq_mod
+#align fin.coe_of_nat_eq_mod Fin.coe_ofNat_eq_mod
 
 section Mul