fixes

Author: kim-em

Mathlib/Algebra/Group/Fin/Basic.lean

@@ -41,7 +41,7 @@ instance addCommMonoid (n : ℕ) [NeZero n] : AddCommMonoid (Fin n) where
 
 instance instAddMonoidWithOne (n) [NeZero n] : AddMonoidWithOne (Fin n) where
   __ := inferInstanceAs (AddCommMonoid (Fin n))
-  natCast i := Fin.ofNat' n i
+  natCast i := Fin.ofNat n i
   natCast_zero := rfl
   natCast_succ _ := Fin.ext (add_mod _ _ _)
 

Mathlib/Control/Random.lean

@@ -96,7 +96,7 @@ def randBound (α : Type u)
 
 /-- Generate a random `Fin`. -/
 def randFin {n : Nat} [NeZero n] [RandomGen g] : RandGT g m (Fin n) :=
-  fun ⟨g⟩ ↦ pure <| randNat g 0 (n - 1) |>.map (Fin.ofNat' n) ULift.up
+  fun ⟨g⟩ ↦ pure <| randNat g 0 (n - 1) |>.map (Fin.ofNat n) ULift.up
 
 instance {n : Nat} [NeZero n] : Random m (Fin n) where
   random := randFin

Mathlib/Data/BitVec.lean

@@ -69,7 +69,7 @@ instance : CommSemiring (BitVec w) :=
   rw [Fin.intCast_def]
   split <;> rename_i h
   · simp [Int.emod_natAbs_of_nonneg h]
-  · simp only [Fin.ofNat'_eq_cast, Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]
+  · simp only [Fin.ofNat_eq_cast, Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]
     split <;> rename_i h
     · rw [← Int.natCast_dvd] at h
       rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]

Mathlib/Data/Fin/Basic.lean

@@ -315,7 +315,7 @@ theorem default_eq_zero (n : ℕ) [NeZero n] : (default : Fin n) = 0 :=
   rfl
 
 instance instNatCast [NeZero n] : NatCast (Fin n) where
-  natCast i := Fin.ofNat' n i
+  natCast i := Fin.ofNat n i
 
 lemma natCast_def [NeZero n] (a : ℕ) : (a : Fin n) = ⟨a % n, mod_lt _ n.pos_of_neZero⟩ := rfl
 
@@ -349,9 +349,12 @@ lemma val_sub_one_of_ne_zero [NeZero n] {i : Fin n} (hi : i ≠ 0) : (i - 1).val
 section OfNatCoe
 
 @[simp]
-theorem ofNat'_eq_cast (n : ℕ) [NeZero n] (a : ℕ) : Fin.ofNat' n a = a :=
+theorem ofNat_eq_cast (n : ℕ) [NeZero n] (a : ℕ) : Fin.ofNat n a = a :=
   rfl
 
+@[deprecated ofNat_eq_cast (since := "2025-05-30")]
+alias ofNat'_eq_cast := ofNat_eq_cast
+
 @[simp] lemma val_natCast (a n : ℕ) [NeZero n] : (a : Fin n).val = a % n := rfl
 
 /-- Converting an in-range number to `Fin (n + 1)` produces a result

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e3a80820ad8cb9c5efcd879b26df954346fc5501",
+   "rev": "33ce662d447121e0a98b1e806b966d3742e0c5b5",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",