chore(Data/Int/Cast): fix confusion between OfNat and Nat.cast le…

…mmas (#11861)

This renames

* `Int.cast_ofNat` to `Int.cast_natCast`
* `Int.int_cast_ofNat` to `Int.cast_ofNat`

I think the history here is that this lemma was previously about `Int.ofNat`, before we globally fixed the simp-normal form to be `Nat.cast`.

Since the `Int.cast_ofNat` name is repurposed, it can't be deprecated. `Int.int_cast_ofNat` is such a wonky name that it was probably never used.

Mathlib/Algebra/Algebra/Basic.lean

@@ -592,7 +592,7 @@ def semiringToRing [Semiring A] [Algebra R A] : Ring A :=
   { __ := (inferInstance : Semiring A)
     __ := Module.addCommMonoidToAddCommGroup R
     intCast := fun z => algebraMap R A z
-    intCast_ofNat := fun z => by simp only [Int.cast_ofNat, map_natCast]
+    intCast_ofNat := fun z => by simp only [Int.cast_natCast, map_natCast]
     intCast_negSucc := fun z => by simp }
 #align algebra.semiring_to_ring Algebra.semiringToRing
 

Mathlib/Algebra/CharP/Basic.lean

@@ -145,10 +145,10 @@ theorem CharP.int_cast_eq_zero_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a
   rcases lt_trichotomy a 0 with (h | rfl | h)
   · rw [← neg_eq_zero, ← Int.cast_neg, ← dvd_neg]
     lift -a to ℕ using neg_nonneg.mpr (le_of_lt h) with b
-    rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
+    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
   · simp only [Int.cast_zero, eq_self_iff_true, dvd_zero]
   · lift a to ℕ using le_of_lt h with b
-    rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
+    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
 #align char_p.int_cast_eq_zero_iff CharP.int_cast_eq_zero_iff
 
 theorem CharP.intCast_eq_intCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℤ} :

Mathlib/Algebra/CharP/MixedCharZero.lean

@@ -229,15 +229,15 @@ noncomputable def algebraRat (h : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸
       intro a b
       field_simp
       trans (↑((a * b).num * a.den * b.den) : R)
-      · simp_rw [Int.cast_mul, Int.cast_ofNat]
+      · simp_rw [Int.cast_mul, Int.cast_natCast]
         ring
       rw [Rat.mul_num_den' a b]
       simp
     map_add' := by
       intro a b
       field_simp
       trans (↑((a + b).num * a.den * b.den) : R)
-      · simp_rw [Int.cast_mul, Int.cast_ofNat]
+      · simp_rw [Int.cast_mul, Int.cast_natCast]
         ring
       rw [Rat.add_num_den' a b]
       simp }

Mathlib/Algebra/CharZero/Quotient.lean

@@ -43,7 +43,7 @@ theorem nsmul_mem_zmultiples_iff_exists_sub_div {r : R} {n : ℕ} (hn : n ≠ 0)
     n • r ∈ AddSubgroup.zmultiples p ↔
       ∃ k : Fin n, r - (k : ℕ) • (p / n : R) ∈ AddSubgroup.zmultiples p := by
   rw [← natCast_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.natCast_ne_zero.mpr hn),
-    Int.cast_ofNat]
+    Int.cast_natCast]
   rfl
 #align add_subgroup.nsmul_mem_zmultiples_iff_exists_sub_div AddSubgroup.nsmul_mem_zmultiples_iff_exists_sub_div
 
@@ -67,7 +67,7 @@ theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {
 theorem zmultiples_nsmul_eq_nsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {n : ℕ} (hz : n ≠ 0) :
     n • ψ = n • θ ↔ ∃ k : Fin n, ψ = θ + (k : ℕ) • (p / n : R) := by
   rw [← natCast_zsmul ψ, ← natCast_zsmul θ,
-    zmultiples_zsmul_eq_zsmul_iff (Int.natCast_ne_zero.mpr hz), Int.cast_ofNat]
+    zmultiples_zsmul_eq_zsmul_iff (Int.natCast_ne_zero.mpr hz), Int.cast_natCast]
   rfl
 #align quotient_add_group.zmultiples_nsmul_eq_nsmul_iff QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff
 

Mathlib/Algebra/DirectSum/Internal.lean

@@ -71,7 +71,7 @@ theorem SetLike.nat_cast_mem_graded [Zero ι] [AddMonoidWithOne R] [SetLike σ R
 theorem SetLike.int_cast_mem_graded [Zero ι] [AddGroupWithOne R] [SetLike σ R]
     [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedOne A] (z : ℤ) : (z : R) ∈ A 0 := by
   induction z
-  · rw [Int.ofNat_eq_coe, Int.cast_ofNat]
+  · rw [Int.ofNat_eq_coe, Int.cast_natCast]
     exact SetLike.nat_cast_mem_graded _ _
   · rw [Int.cast_negSucc]
     exact neg_mem (SetLike.nat_cast_mem_graded _ _)
@@ -122,7 +122,7 @@ instance gring [AddMonoid ι] [Ring R] [SetLike σ R] [AddSubgroupClass σ R] (A
     [SetLike.GradedMonoid A] : DirectSum.GRing fun i => A i :=
   { SetLike.gsemiring A with
     intCast := fun z => ⟨z, SetLike.int_cast_mem_graded _ _⟩
-    intCast_ofNat := fun _n => Subtype.ext <| Int.cast_ofNat _
+    intCast_ofNat := fun _n => Subtype.ext <| Int.cast_natCast _
     intCast_negSucc_ofNat := fun n => Subtype.ext <| Int.cast_negSucc n }
 #align set_like.gring SetLike.gring
 

Mathlib/Algebra/Group/InjSurj.lean

@@ -342,7 +342,7 @@ protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ
   { hf.addGroup f zero add neg sub (swap nsmul) (swap zsmul),
     hf.addMonoidWithOne f zero one add nsmul nat_cast with
     intCast := Int.cast,
-    intCast_ofNat := fun n => hf (by rw [nat_cast, ← Int.cast, int_cast, Int.cast_ofNat]),
+    intCast_ofNat := fun n => hf (by rw [nat_cast, ← Int.cast, int_cast, Int.cast_natCast]),
     intCast_negSucc := fun n => hf (by erw [int_cast, neg, nat_cast, Int.cast_negSucc] ) }
 #align function.injective.add_group_with_one Function.Injective.addGroupWithOne
 
@@ -553,7 +553,7 @@ protected def addGroupWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [Neg M₂
   { hf.addMonoidWithOne f zero one add nsmul nat_cast,
     hf.addGroup f zero add neg sub (swap nsmul) (swap zsmul) with
     intCast := Int.cast,
-    intCast_ofNat := fun n => by rw [← Int.cast, ← int_cast, Int.cast_ofNat, nat_cast],
+    intCast_ofNat := fun n => by rw [← Int.cast, ← int_cast, Int.cast_natCast, nat_cast],
     intCast_negSucc := fun n => by
       rw [← Int.cast, ← int_cast, Int.cast_negSucc, neg, nat_cast] }
 #align function.surjective.add_group_with_one Function.Surjective.addGroupWithOne

Mathlib/Algebra/Group/Opposite.lean

@@ -76,7 +76,7 @@ instance instAddGroupWithOne [AddGroupWithOne α] : AddGroupWithOne αᵐᵒᵖ
   toAddMonoidWithOne := instAddMonoidWithOne
   toIntCast := instIntCast
   __ := instAddGroup
-  intCast_ofNat n := show op ((n : ℤ) : α) = op (n : α) by rw [Int.cast_ofNat]
+  intCast_ofNat n := show op ((n : ℤ) : α) = op (n : α) by rw [Int.cast_natCast]
   intCast_negSucc n := show op _ = op (-unop (op ((n + 1 : ℕ) : α))) by simp
 
 instance instAddCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne αᵐᵒᵖ where
@@ -388,7 +388,7 @@ instance instAddCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne
   toIntCast := instIntCast
   toAddCommGroup := instAddCommGroup
   __ := instAddCommMonoidWithOne
-  intCast_ofNat _ := congr_arg op <| Int.cast_ofNat _
+  intCast_ofNat _ := congr_arg op <| Int.cast_natCast _
   intCast_negSucc _ := congr_arg op <| Int.cast_negSucc _
 
 /-- The function `AddOpposite.op` is a multiplicative equivalence. -/

Mathlib/Algebra/Group/ULift.lean

@@ -223,7 +223,7 @@ instance commGroup [CommGroup α] : CommGroup (ULift α) :=
 instance addGroupWithOne [AddGroupWithOne α] : AddGroupWithOne (ULift α) :=
   { ULift.addMonoidWithOne, ULift.addGroup with
       intCast := (⟨·⟩),
-      intCast_ofNat := fun _ => congr_arg ULift.up (Int.cast_ofNat _),
+      intCast_ofNat := fun _ => congr_arg ULift.up (Int.cast_natCast _),
       intCast_negSucc := fun _ => congr_arg ULift.up (Int.cast_negSucc _) }
 #align ulift.add_group_with_one ULift.addGroupWithOne
 

Mathlib/Algebra/ModEq.lean

@@ -329,7 +329,7 @@ lemma intCast_modEq_intCast' {a b : ℤ} {n : ℕ} : a ≡ b [PMOD (n : α)] ↔
 @[simp, norm_cast]
 theorem natCast_modEq_natCast {a b n : ℕ} : a ≡ b [PMOD (n : α)] ↔ a ≡ b [MOD n] := by
   simp_rw [← Int.natCast_modEq_iff, ← modEq_iff_int_modEq, ← @intCast_modEq_intCast α,
-    Int.cast_ofNat]
+    Int.cast_natCast]
 #align add_comm_group.nat_cast_modeq_nat_cast AddCommGroup.natCast_modEq_natCast
 
 alias ⟨ModEq.of_intCast, ModEq.intCast⟩ := intCast_modEq_intCast

Mathlib/Algebra/Order/Archimedean.lean

@@ -162,7 +162,7 @@ variable [StrictOrderedRing α] [Archimedean α]
 
 theorem exists_int_gt (x : α) : ∃ n : ℤ, x < n :=
   let ⟨n, h⟩ := exists_nat_gt x
-  ⟨n, by rwa [Int.cast_ofNat]⟩
+  ⟨n, by rwa [Int.cast_natCast]⟩
 #align exists_int_gt exists_int_gt
 
 theorem exists_int_lt (x : α) : ∃ n : ℤ, (n : α) < x :=
@@ -299,7 +299,7 @@ theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q : α)
   · rw [Rat.coe_int_den, Nat.cast_one]
     exact one_ne_zero
   · intro H
-    rw [Rat.num_natCast, Int.cast_ofNat, Nat.cast_eq_zero] at H
+    rw [Rat.num_natCast, Int.cast_natCast, Nat.cast_eq_zero] at H
     subst H
     cases n0
   · rw [Rat.den_natCast, Nat.cast_one]

Mathlib/Algebra/Order/Floor.lean

@@ -731,7 +731,7 @@ theorem floor_intCast (z : ℤ) : ⌊(z : α)⌋ = z :=
 
 @[simp]
 theorem floor_natCast (n : ℕ) : ⌊(n : α)⌋ = n :=
-  eq_of_forall_le_iff fun a => by rw [le_floor, ← cast_ofNat, cast_le]
+  eq_of_forall_le_iff fun a => by rw [le_floor, ← cast_natCast, cast_le]
 #align int.floor_nat_cast Int.floor_natCast
 
 @[simp]
@@ -789,7 +789,8 @@ theorem floor_int_add (z : ℤ) (a : α) : ⌊↑z + a⌋ = z + ⌊a⌋ := by
 #align int.floor_int_add Int.floor_int_add
 
 @[simp]
-theorem floor_add_nat (a : α) (n : ℕ) : ⌊a + n⌋ = ⌊a⌋ + n := by rw [← Int.cast_ofNat, floor_add_int]
+theorem floor_add_nat (a : α) (n : ℕ) : ⌊a + n⌋ = ⌊a⌋ + n := by
+  rw [← Int.cast_natCast, floor_add_int]
 #align int.floor_add_nat Int.floor_add_nat
 
 -- See note [no_index around OfNat.ofNat]
@@ -800,7 +801,7 @@ theorem floor_add_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
 
 @[simp]
 theorem floor_nat_add (n : ℕ) (a : α) : ⌊↑n + a⌋ = n + ⌊a⌋ := by
-  rw [← Int.cast_ofNat, floor_int_add]
+  rw [← Int.cast_natCast, floor_int_add]
 #align int.floor_nat_add Int.floor_nat_add
 
 -- See note [no_index around OfNat.ofNat]
@@ -815,7 +816,8 @@ theorem floor_sub_int (a : α) (z : ℤ) : ⌊a - z⌋ = ⌊a⌋ - z :=
 #align int.floor_sub_int Int.floor_sub_int
 
 @[simp]
-theorem floor_sub_nat (a : α) (n : ℕ) : ⌊a - n⌋ = ⌊a⌋ - n := by rw [← Int.cast_ofNat, floor_sub_int]
+theorem floor_sub_nat (a : α) (n : ℕ) : ⌊a - n⌋ = ⌊a⌋ - n := by
+  rw [← Int.cast_natCast, floor_sub_int]
 #align int.floor_sub_nat Int.floor_sub_nat
 
 @[simp] theorem floor_sub_one (a : α) : ⌊a - 1⌋ = ⌊a⌋ - 1 := mod_cast floor_sub_nat a 1
@@ -1151,7 +1153,7 @@ theorem fract_div_intCast_eq_div_intCast_mod {m : ℤ} {n : ℕ} :
   have : ∀ {l : ℤ}, 0 ≤ l → fract ((l : k) / n) = ↑(l % n) / n := by
     intros l hl
     obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg
-    · rw [cast_ofNat, ← natCast_mod, cast_ofNat, fract_div_natCast_eq_div_natCast_mod]
+    · rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]
     · rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl
       simp [hl, zero_mod]
   obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg
@@ -1162,8 +1164,8 @@ theorem fract_div_intCast_eq_div_intCast_mod {m : ℤ} {n : ℕ} :
     simpa [m₁, ← @cast_le k, ← div_le_iff hn] using FloorRing.gc_ceil_coe.le_u_l _
   calc
     fract ((Int.cast (-(m₀ : ℤ)) : k) / (n : k))
-      -- Porting note: the `rw [cast_neg, cast_ofNat]` was `push_cast`
-      = fract (-(m₀ : k) / n) := by rw [cast_neg, cast_ofNat]
+      -- Porting note: the `rw [cast_neg, cast_natCast]` was `push_cast`
+      = fract (-(m₀ : k) / n) := by rw [cast_neg, cast_natCast]
     _ = fract ((m₁ : k) / n) := ?_
     _ = Int.cast (m₁ % (n : ℤ)) / Nat.cast n := this hm₁
     _ = Int.cast (-(↑m₀ : ℤ) % ↑n) / Nat.cast n := ?_
@@ -1225,7 +1227,7 @@ theorem ceil_intCast (z : ℤ) : ⌈(z : α)⌉ = z :=
 
 @[simp]
 theorem ceil_natCast (n : ℕ) : ⌈(n : α)⌉ = n :=
-  eq_of_forall_ge_iff fun a => by rw [ceil_le, ← cast_ofNat, cast_le]
+  eq_of_forall_ge_iff fun a => by rw [ceil_le, ← cast_natCast, cast_le]
 #align int.ceil_nat_cast Int.ceil_natCast
 
 -- See note [no_index around OfNat.ofNat]
@@ -1245,7 +1247,7 @@ theorem ceil_add_int (a : α) (z : ℤ) : ⌈a + z⌉ = ⌈a⌉ + z := by
 #align int.ceil_add_int Int.ceil_add_int
 
 @[simp]
-theorem ceil_add_nat (a : α) (n : ℕ) : ⌈a + n⌉ = ⌈a⌉ + n := by rw [← Int.cast_ofNat, ceil_add_int]
+theorem ceil_add_nat (a : α) (n : ℕ) : ⌈a + n⌉ = ⌈a⌉ + n := by rw [← Int.cast_natCast, ceil_add_int]
 #align int.ceil_add_nat Int.ceil_add_nat
 
 @[simp]
@@ -1689,8 +1691,8 @@ instance (priority := 100) FloorRing.toFloorSemiring : FloorSemiring α where
   floor a := ⌊a⌋.toNat
   ceil a := ⌈a⌉.toNat
   floor_of_neg {a} ha := Int.toNat_of_nonpos (Int.floor_nonpos ha.le)
-  gc_floor {a n} ha := by rw [Int.le_toNat (Int.floor_nonneg.2 ha), Int.le_floor, Int.cast_ofNat]
-  gc_ceil a n := by rw [Int.toNat_le, Int.ceil_le, Int.cast_ofNat]
+  gc_floor {a n} ha := by rw [Int.le_toNat (Int.floor_nonneg.2 ha), Int.le_floor, Int.cast_natCast]
+  gc_ceil a n := by rw [Int.toNat_le, Int.ceil_le, Int.cast_natCast]
 #align floor_ring.to_floor_semiring FloorRing.toFloorSemiring
 
 theorem Int.floor_toNat (a : α) : ⌊a⌋.toNat = ⌊a⌋₊ :=
@@ -1722,11 +1724,11 @@ theorem Int.ofNat_ceil_eq_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : ℤ) = ⌈a⌉ :=
 #align nat.cast_ceil_eq_int_ceil Int.ofNat_ceil_eq_ceil
 
 theorem natCast_floor_eq_intCast_floor (ha : 0 ≤ a) : (⌊a⌋₊ : α) = ⌊a⌋ := by
-  rw [← Int.ofNat_floor_eq_floor ha, Int.cast_ofNat]
+  rw [← Int.ofNat_floor_eq_floor ha, Int.cast_natCast]
 #align nat.cast_floor_eq_cast_int_floor natCast_floor_eq_intCast_floor
 
 theorem natCast_ceil_eq_intCast_ceil  (ha : 0 ≤ a) : (⌈a⌉₊ : α) = ⌈a⌉ := by
-  rw [← Int.ofNat_ceil_eq_ceil ha, Int.cast_ofNat]
+  rw [← Int.ofNat_ceil_eq_ceil ha, Int.cast_natCast]
 #align nat.cast_ceil_eq_cast_int_ceil natCast_ceil_eq_intCast_ceil
 
 -- 2024-02-14

Mathlib/Algebra/Periodic.lean

@@ -451,7 +451,7 @@ theorem Antiperiodic.nat_mul_eq_of_eq_zero [Semiring α] [NegZeroClass β] (h :
 
 theorem Antiperiodic.int_mul_eq_of_eq_zero [Ring α] [SubtractionMonoid β] (h : Antiperiodic f c)
     (hi : f 0 = 0) : ∀ n : ℤ, f (n * c) = 0
-  | (n : ℕ) => by rw [Int.cast_ofNat, h.nat_mul_eq_of_eq_zero hi n]
+  | (n : ℕ) => by rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]
   | .negSucc n => by rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]
 #align function.antiperiodic.int_mul_eq_of_eq_zero Function.Antiperiodic.int_mul_eq_of_eq_zero
 

Mathlib/Algebra/Quaternion.lean

@@ -400,7 +400,7 @@ instance : AddCommGroupWithOne ℍ[R,c₁,c₂] where
   natCast_zero := by simp
   natCast_succ := by simp
   intCast n := ((n : R) : ℍ[R,c₁,c₂])
-  intCast_ofNat _ := congr_arg coe (Int.cast_ofNat _)
+  intCast_ofNat _ := congr_arg coe (Int.cast_natCast _)
   intCast_negSucc n := by
     change coe _ = -coe _
     rw [Int.cast_negSucc, coe_neg]

Mathlib/Algebra/RingQuot.lean

@@ -374,7 +374,7 @@ instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot
       simp [smul_quot, neg_quot, add_mul]
     intCast := intCast r
     intCast_ofNat := fun n => congrArg RingQuot.mk <| by
-      exact congrArg (Quot.mk _) (Int.cast_ofNat _)
+      exact congrArg (Quot.mk _) (Int.cast_natCast _)
     intCast_negSucc := fun n => congrArg RingQuot.mk <| by
       simp_rw [neg_def]
       exact congrArg (Quot.mk _) (Int.cast_negSucc n) }

Mathlib/Algebra/Star/CHSH.lean

@@ -205,7 +205,7 @@ theorem tsirelson_inequality [OrderedRing R] [StarRing R] [StarOrderedRing R] [A
     -- all terms coincide, but the last one. Simplify all other terms
     simp only [M]
     simp only [neg_mul, one_mul, mul_inv_cancel_of_invertible, Int.cast_one, add_assoc, add_comm,
-      add_left_comm, one_smul, Int.cast_neg, neg_smul, Int.int_cast_ofNat]
+      add_left_comm, one_smul, Int.cast_neg, neg_smul, Int.cast_ofNat]
     simp only [← add_assoc, ← add_smul]
     -- just look at the coefficients now:
     congr

Mathlib/Algebra/TrivSqZeroExt.lean

@@ -548,7 +548,7 @@ theorem inl_nat_cast [AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : (inl n : tsz
 instance addGroupWithOne [AddGroupWithOne R] [AddGroup M] : AddGroupWithOne (tsze R M) :=
   { TrivSqZeroExt.addGroup, TrivSqZeroExt.addMonoidWithOne with
     intCast := fun z => inl z
-    intCast_ofNat := fun _n => ext (Int.cast_ofNat _) rfl
+    intCast_ofNat := fun _n => ext (Int.cast_natCast _) rfl
     intCast_negSucc := fun _n => ext (Int.cast_negSucc _) neg_zero.symm }
 
 @[simp]

Mathlib/Analysis/Calculus/Deriv/ZPow.lean

@@ -40,7 +40,7 @@ theorem hasStrictDerivAt_zpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
     HasStrictDerivAt (fun x => x ^ m) ((m : 𝕜) * x ^ (m - 1)) x := by
   have : ∀ m : ℤ, 0 < m → HasStrictDerivAt (· ^ m) ((m : 𝕜) * x ^ (m - 1)) x := fun m hm ↦ by
     lift m to ℕ using hm.le
-    simp only [zpow_natCast, Int.cast_ofNat]
+    simp only [zpow_natCast, Int.cast_natCast]
     convert hasStrictDerivAt_pow m x using 2
     rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_natCast]
     norm_cast at hm
@@ -110,7 +110,7 @@ theorem iter_deriv_zpow' (m : ℤ) (k : ℕ) :
   · simp only [Nat.zero_eq, one_mul, Int.ofNat_zero, id, sub_zero, Finset.prod_range_zero,
       Function.iterate_zero]
   · simp only [Function.iterate_succ_apply', ihk, deriv_const_mul_field', deriv_zpow',
-      Finset.prod_range_succ, Int.ofNat_succ, ← sub_sub, Int.cast_sub, Int.cast_ofNat, mul_assoc]
+      Finset.prod_range_succ, Int.ofNat_succ, ← sub_sub, Int.cast_sub, Int.cast_natCast, mul_assoc]
 #align iter_deriv_zpow' iter_deriv_zpow'
 
 theorem iter_deriv_zpow (m : ℤ) (x : 𝕜) (k : ℕ) :
@@ -120,7 +120,7 @@ theorem iter_deriv_zpow (m : ℤ) (x : 𝕜) (k : ℕ) :
 
 theorem iter_deriv_pow (n : ℕ) (x : 𝕜) (k : ℕ) :
     deriv^[k] (fun x : 𝕜 => x ^ n) x = (∏ i in Finset.range k, ((n : 𝕜) - i)) * x ^ (n - k) := by
-  simp only [← zpow_natCast, iter_deriv_zpow, Int.cast_ofNat]
+  simp only [← zpow_natCast, iter_deriv_zpow, Int.cast_natCast]
   rcases le_or_lt k n with hkn | hnk
   · rw [Int.ofNat_sub hkn]
   · have : (∏ i in Finset.range k, (n - i : 𝕜)) = 0 :=

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -164,7 +164,7 @@ theorem isBigO_cocompact_rpow [ProperSpace E] (s : ℝ) :
   refine' ⟨1, (Filter.eventually_ge_atTop 1).mono fun x hx => _⟩
   rw [one_mul, Real.norm_of_nonneg (Real.rpow_nonneg (zero_le_one.trans hx) _),
     Real.norm_of_nonneg (zpow_nonneg (zero_le_one.trans hx) _), ← Real.rpow_int_cast, Int.cast_neg,
-    Int.cast_ofNat]
+    Int.cast_natCast]
   exact Real.rpow_le_rpow_of_exponent_le hx hk
 set_option linter.uppercaseLean3 false in
 #align schwartz_map.is_O_cocompact_rpow SchwartzMap.isBigO_cocompact_rpow

Mathlib/Analysis/InnerProductSpace/OfNorm.lean

@@ -255,7 +255,7 @@ private theorem nat_prop (r : ℕ) : innerProp' E (r : 𝕜) := fun x y => by
 private theorem int_prop (n : ℤ) : innerProp' E (n : 𝕜) := by
   intro x y
   rw [← n.sign_mul_natAbs]
-  simp only [Int.cast_ofNat, map_natCast, map_intCast, Int.cast_mul, map_mul, mul_smul]
+  simp only [Int.cast_natCast, map_natCast, map_intCast, Int.cast_mul, map_mul, mul_smul]
   obtain hn | rfl | hn := lt_trichotomy n 0
   · rw [Int.sign_eq_neg_one_of_neg hn, innerProp_neg_one ((n.natAbs : 𝕜) • x), nat]
     simp only [map_neg, neg_mul, one_mul, mul_eq_mul_left_iff, true_or_iff, Int.natAbs_eq_zero,

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -1928,7 +1928,8 @@ theorem norm_coe_nat (n : ℕ) : ‖(n : ℤ)‖ = n := by simp [Int.norm_eq_abs
 theorem _root_.NNReal.natCast_natAbs (n : ℤ) : (n.natAbs : ℝ≥0) = ‖n‖₊ :=
   NNReal.eq <|
     calc
-      ((n.natAbs : ℝ≥0) : ℝ) = (n.natAbs : ℤ) := by simp only [Int.cast_ofNat, NNReal.coe_nat_cast]
+      ((n.natAbs : ℝ≥0) : ℝ) = (n.natAbs : ℤ) := by
+        simp only [Int.cast_natCast, NNReal.coe_nat_cast]
       _ = |(n : ℝ)| := by simp only [Int.natCast_natAbs, Int.cast_abs]
       _ = ‖n‖ := (norm_eq_abs n).symm
 #align nnreal.coe_nat_abs NNReal.natCast_natAbs