chore: Rename zpow_coe_nat to zpow_natCast (#11528)

... and add a deprecated alias for the old name. This is mostly just me discovering the power of `F2`

Mathlib/Algebra/CharZero/Quotient.lean

@@ -25,7 +25,7 @@ theorem zsmul_mem_zmultiples_iff_exists_sub_div {r : R} {z : ℤ} (hz : z ≠ 0)
   have hz' : (z : R) ≠ 0 := Int.cast_ne_zero.mpr hz
   conv_rhs => simp (config := { singlePass := true }) only [← (mul_right_injective₀ hz').eq_iff]
   simp_rw [← zsmul_eq_mul, smul_add, ← mul_smul_comm, zsmul_eq_mul (z : R)⁻¹, mul_inv_cancel hz',
-    mul_one, ← coe_nat_zsmul, smul_smul, ← add_smul]
+    mul_one, ← natCast_zsmul, smul_smul, ← add_smul]
   constructor
   · rintro ⟨k, h⟩
     simp_rw [← h]
@@ -42,7 +42,7 @@ theorem zsmul_mem_zmultiples_iff_exists_sub_div {r : R} {z : ℤ} (hz : z ≠ 0)
 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 [← coe_nat_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.coe_nat_ne_zero.mpr hn),
+  rw [← natCast_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.coe_nat_ne_zero.mpr hn),
     Int.cast_ofNat]
   rfl
 #align add_subgroup.nsmul_mem_zmultiples_iff_exists_sub_div AddSubgroup.nsmul_mem_zmultiples_iff_exists_sub_div
@@ -66,7 +66,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 [← coe_nat_zsmul ψ, ← coe_nat_zsmul θ,
+  rw [← natCast_zsmul ψ, ← natCast_zsmul θ,
     zmultiples_zsmul_eq_zsmul_iff (Int.coe_nat_ne_zero.mpr hz), Int.cast_ofNat]
   rfl
 #align quotient_add_group.zmultiples_nsmul_eq_nsmul_iff QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff

Mathlib/Algebra/Group/Conj.lean

@@ -113,10 +113,10 @@ theorem conj_pow {i : ℕ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻
 theorem conj_zpow {i : ℤ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹ := by
   induction' i
   · change (a * b * a⁻¹) ^ (_ : ℤ) = a * b ^ (_ : ℤ) * a⁻¹
-    simp [zpow_coe_nat]
+    simp [zpow_natCast]
   · simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
     rw [mul_assoc]
--- Porting note: Added `change`, `zpow_coe_nat`, and `rw`.
+-- Porting note: Added `change`, `zpow_natCast`, and `rw`.
 #align conj_zpow conj_zpow
 
 theorem conj_injective {x : α} : Function.Injective fun g : α => x * g * x⁻¹ :=

Mathlib/Algebra/Group/Defs.lean

@@ -958,31 +958,35 @@ variable [DivInvMonoid G] {a b : G}
 #align zpow_zero zpow_zero
 #align zero_zsmul zero_zsmul
 
-@[to_additive (attr := simp, norm_cast) coe_nat_zsmul]
-theorem zpow_coe_nat (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
+@[to_additive (attr := simp, norm_cast) natCast_zsmul]
+theorem zpow_natCast (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
   | 0 => (zpow_zero _).trans (pow_zero _).symm
   | n + 1 => calc
     a ^ (↑(n + 1) : ℤ) = a * a ^ (n : ℤ) := DivInvMonoid.zpow_succ' _ _
-    _ = a * a ^ n := congrArg (a * ·) (zpow_coe_nat a n)
+    _ = a * a ^ n := congrArg (a * ·) (zpow_natCast a n)
     _ = a ^ (n + 1) := (pow_succ _ _).symm
-#align zpow_coe_nat zpow_coe_nat
-#align zpow_of_nat zpow_coe_nat
-#align coe_nat_zsmul coe_nat_zsmul
-#align of_nat_zsmul coe_nat_zsmul
+#align zpow_coe_nat zpow_natCast
+#align zpow_of_nat zpow_natCast
+#align coe_nat_zsmul natCast_zsmul
+#align of_nat_zsmul natCast_zsmul
+
+-- 2024-03-20
+@[deprecated] alias zpow_coe_nat := zpow_natCast
+@[deprecated] alias coe_nat_zsmul := natCast_zsmul
 
 -- See note [no_index around OfNat.ofNat]
 @[to_additive ofNat_zsmul]
 lemma zpow_ofNat (a : G) (n : ℕ) : a ^ (no_index (OfNat.ofNat n) : ℤ) = a ^ OfNat.ofNat n :=
-  zpow_coe_nat ..
+  zpow_natCast ..
 
 theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ := by
-  rw [← zpow_coe_nat]
+  rw [← zpow_natCast]
   exact DivInvMonoid.zpow_neg' n a
 #align zpow_neg_succ_of_nat zpow_negSucc
 
 theorem negSucc_zsmul {G} [SubNegMonoid G] (a : G) (n : ℕ) :
     Int.negSucc n • a = -((n + 1) • a) := by
-  rw [← coe_nat_zsmul]
+  rw [← natCast_zsmul]
   exact SubNegMonoid.zsmul_neg' n a
 #align zsmul_neg_succ_of_nat negSucc_zsmul
 

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -480,7 +480,7 @@ lemma map_comp_pow [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (
 @[to_additive]
 theorem map_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H]
     (f : F) (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹) (a : G) : ∀ n : ℤ, f (a ^ n) = f a ^ n
-  | (n : ℕ) => by rw [zpow_coe_nat, map_pow, zpow_coe_nat]
+  | (n : ℕ) => by rw [zpow_natCast, map_pow, zpow_natCast]
   | Int.negSucc n => by rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]
 #align map_zpow' map_zpow'
 #align map_zsmul' map_zsmul'

Mathlib/Algebra/Group/Hom/Instances.lean

@@ -68,10 +68,10 @@ instance MonoidHom.commGroup {M G} [MulOneClass M] [CommGroup G] : CommGroup (M
       simp,
     zpow_succ' := fun n f => by
       ext x
-      simp [zpow_coe_nat, pow_succ],
+      simp [zpow_natCast, pow_succ],
     zpow_neg' := fun n f => by
       ext x
-      simp [Nat.succ_eq_add_one, zpow_coe_nat, -Int.natCast_add] }
+      simp [Nat.succ_eq_add_one, zpow_natCast, -Int.natCast_add] }
 
 instance AddMonoid.End.instAddCommMonoid [AddCommMonoid M] : AddCommMonoid (AddMonoid.End M) :=
   AddMonoidHom.addCommMonoid
@@ -113,7 +113,7 @@ instance AddMonoid.End.instAddCommGroup [AddCommGroup M] : AddCommGroup (AddMono
 instance AddMonoid.End.instRing [AddCommGroup M] : Ring (AddMonoid.End M) :=
   { AddMonoid.End.instSemiring, AddMonoid.End.instAddCommGroup with
     intCast := fun z => z • (1 : AddMonoid.End M),
-    intCast_ofNat := coe_nat_zsmul _,
+    intCast_ofNat := natCast_zsmul _,
     intCast_negSucc := negSucc_zsmul _ }
 
 /-- See also `AddMonoid.End.intCast_def`. -/

Mathlib/Algebra/Group/InjSurj.lean

@@ -250,8 +250,8 @@ protected def divInvMonoid [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injecti
   { hf.monoid f one mul npow, ‹Inv M₁›, ‹Div M₁› with
     zpow := fun n x => x ^ n,
     zpow_zero' := fun x => hf <| by erw [zpow, zpow_zero, one],
-    zpow_succ' := fun n x => hf <| by erw [zpow, mul, zpow_coe_nat, pow_succ, zpow, zpow_coe_nat],
-    zpow_neg' := fun n x => hf <| by erw [zpow, zpow_negSucc, inv, zpow, zpow_coe_nat],
+    zpow_succ' := fun n x => hf <| by erw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast],
+    zpow_neg' := fun n x => hf <| by erw [zpow, zpow_negSucc, inv, zpow, zpow_natCast],
     div_eq_mul_inv := fun x y => hf <| by erw [div, mul, inv, div_eq_mul_inv] }
 #align function.injective.div_inv_monoid Function.Injective.divInvMonoid
 #align function.injective.sub_neg_monoid Function.Injective.subNegMonoid
@@ -506,10 +506,10 @@ protected def divInvMonoid [DivInvMonoid M₁] (f : M₁ → M₂) (hf : Surject
     zpow_zero' := hf.forall.2 fun x => by dsimp only; erw [← zpow, zpow_zero, ← one],
     zpow_succ' := fun n => hf.forall.2 fun x => by
       dsimp only
-      erw [← zpow, ← zpow, zpow_coe_nat, zpow_coe_nat, pow_succ, ← mul],
+      erw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul],
     zpow_neg' := fun n => hf.forall.2 fun x => by
       dsimp only
-      erw [← zpow, ← zpow, zpow_negSucc, zpow_coe_nat, inv],
+      erw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv],
     div_eq_mul_inv := hf.forall₂.2 fun x y => by erw [← inv, ← mul, ← div, div_eq_mul_inv] }
 #align function.surjective.div_inv_monoid Function.Surjective.divInvMonoid
 #align function.surjective.sub_neg_monoid Function.Surjective.subNegMonoid

Mathlib/Algebra/Group/Opposite.lean

@@ -158,7 +158,7 @@ instance divInvMonoid [DivInvMonoid α] : DivInvMonoid αᵐᵒᵖ :=
     zpow_zero' := fun x => unop_injective <| DivInvMonoid.zpow_zero' x.unop,
     zpow_succ' := fun n x => unop_injective <| by
       simp only [Int.ofNat_eq_coe]
-      rw [unop_op, zpow_coe_nat, pow_succ', unop_mul, unop_op, zpow_coe_nat],
+      rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast],
     zpow_neg' := fun z x => unop_injective <| DivInvMonoid.zpow_neg' z x.unop }
 
 @[to_additive AddOpposite.subtractionMonoid]

Mathlib/Algebra/Group/Semiconj/Units.lean

@@ -92,7 +92,7 @@ theorem units_val_iff {a x y : Mˣ} : SemiconjBy (a : M) x y ↔ SemiconjBy a x
 @[to_additive (attr := simp)]
 lemma units_zpow_right {a : M} {x y : Mˣ} (h : SemiconjBy a x y) :
     ∀ m : ℤ, SemiconjBy a ↑(x ^ m) ↑(y ^ m)
-  | (n : ℕ) => by simp only [zpow_coe_nat, Units.val_pow_eq_pow_val, h, pow_right]
+  | (n : ℕ) => by simp only [zpow_natCast, Units.val_pow_eq_pow_val, h, pow_right]
   | -[n+1] => by simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]
 #align semiconj_by.units_zpow_right SemiconjBy.units_zpow_right
 #align add_semiconj_by.add_units_zsmul_right AddSemiconjBy.addUnits_zsmul_right

Mathlib/Algebra/GroupPower/Basic.lean

@@ -245,14 +245,14 @@ open Int
 @[to_additive (attr := simp) one_zsmul]
 theorem zpow_one (a : G) : a ^ (1 : ℤ) = a := by
   convert pow_one a using 1
-  exact zpow_coe_nat a 1
+  exact zpow_natCast a 1
 #align zpow_one zpow_one
 #align one_zsmul one_zsmul
 
 @[to_additive two_zsmul]
 theorem zpow_two (a : G) : a ^ (2 : ℤ) = a * a := by
   convert pow_two a using 1
-  exact zpow_coe_nat a 2
+  exact zpow_natCast a 2
 #align zpow_two zpow_two
 #align two_zsmul two_zsmul
 
@@ -284,7 +284,7 @@ theorem inv_pow (a : α) : ∀ n : ℕ, a⁻¹ ^ n = (a ^ n)⁻¹
 -- the attributes are intentionally out of order. `smul_zero` proves `zsmul_zero`.
 @[to_additive zsmul_zero, simp]
 theorem one_zpow : ∀ n : ℤ, (1 : α) ^ n = 1
-  | (n : ℕ)       => by rw [zpow_coe_nat, one_pow]
+  | (n : ℕ)       => by rw [zpow_natCast, one_pow]
   | .negSucc n => by rw [zpow_negSucc, one_pow, inv_one]
 #align one_zpow one_zpow
 #align zsmul_zero zsmul_zero
@@ -296,7 +296,7 @@ theorem zpow_neg (a : α) : ∀ n : ℤ, a ^ (-n) = (a ^ n)⁻¹
     change a ^ (0 : ℤ) = (a ^ (0 : ℤ))⁻¹
     simp
   | Int.negSucc n => by
-    rw [zpow_negSucc, inv_inv, ← zpow_coe_nat]
+    rw [zpow_negSucc, inv_inv, ← zpow_natCast]
     rfl
 #align zpow_neg zpow_neg
 #align neg_zsmul neg_zsmul
@@ -309,7 +309,7 @@ theorem mul_zpow_neg_one (a b : α) : (a * b) ^ (-1 : ℤ) = b ^ (-1 : ℤ) * a
 
 @[to_additive zsmul_neg]
 theorem inv_zpow (a : α) : ∀ n : ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
-  | (n : ℕ)    => by rw [zpow_coe_nat, zpow_coe_nat, inv_pow]
+  | (n : ℕ)    => by rw [zpow_natCast, zpow_natCast, inv_pow]
   | .negSucc n => by rw [zpow_negSucc, zpow_negSucc, inv_pow]
 #align inv_zpow inv_zpow
 #align zsmul_neg zsmul_neg
@@ -331,7 +331,7 @@ theorem one_div_zpow (a : α) (n : ℤ) : (1 / a) ^ n = 1 / a ^ n := by simp onl
 
 @[to_additive AddCommute.zsmul_add]
 protected theorem Commute.mul_zpow (h : Commute a b) : ∀ i : ℤ, (a * b) ^ i = a ^ i * b ^ i
-  | (n : ℕ)    => by simp [zpow_coe_nat, h.mul_pow n]
+  | (n : ℕ)    => by simp [zpow_natCast, h.mul_pow n]
   | .negSucc n => by simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]
 #align commute.mul_zpow Commute.mul_zpow
 #align add_commute.zsmul_add AddCommute.zsmul_add
@@ -341,17 +341,17 @@ protected theorem Commute.mul_zpow (h : Commute a b) : ∀ i : ℤ, (a * b) ^ i
 -- and therefore the more "natural" choice of lemma, is reversed.
 @[to_additive mul_zsmul'] lemma zpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
   | (m : ℕ), (n : ℕ) => by
-    rw [zpow_coe_nat, zpow_coe_nat, ← pow_mul, ← zpow_coe_nat]
+    rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast]
     rfl
   | (m : ℕ), -[n+1] => by
-    rw [zpow_coe_nat, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
-      ← zpow_coe_nat]
+    rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
+      ← zpow_natCast]
   | -[m+1], (n : ℕ) => by
-    rw [zpow_coe_nat, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
-      inv_inj, ← zpow_coe_nat]
+    rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
+      inv_inj, ← zpow_natCast]
   | -[m+1], -[n+1] => by
     rw [zpow_negSucc, zpow_negSucc, Int.negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ←
-      zpow_coe_nat]
+      zpow_natCast]
     rfl
 #align zpow_mul zpow_mul
 #align mul_zsmul' mul_zsmul'
@@ -365,7 +365,7 @@ set_option linter.deprecated false
 
 @[to_additive bit0_zsmul]
 lemma zpow_bit0 (a : α) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n := by
-  rw [bit0, ← Int.two_mul, zpow_mul', ← pow_two, ← zpow_coe_nat]; norm_cast
+  rw [bit0, ← Int.two_mul, zpow_mul', ← pow_two, ← zpow_natCast]; norm_cast
 #align zpow_bit0 zpow_bit0
 #align bit0_zsmul bit0_zsmul
 
@@ -425,7 +425,7 @@ theorem inv_pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^
 
 @[to_additive add_one_zsmul]
 lemma zpow_add_one (a : G) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
-  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_coe_nat, pow_succ']
+  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_natCast, pow_succ']
   | -[0+1] => by simp [Int.negSucc_eq', Int.add_left_neg]
   | -[n + 1+1] => by
     rw [zpow_negSucc, pow_succ, mul_inv_rev, inv_mul_cancel_right]
@@ -537,7 +537,7 @@ end Group
 @[to_additive (attr := simp)]
 theorem SemiconjBy.zpow_right [Group G] {a x y : G} (h : SemiconjBy a x y) :
     ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)
-  | (n : ℕ)    => by simp [zpow_coe_nat, h.pow_right n]
+  | (n : ℕ)    => by simp [zpow_natCast, h.pow_right n]
   | .negSucc n => by
     simp only [zpow_negSucc, inv_right_iff]
     apply pow_right h

Mathlib/Algebra/GroupPower/CovariantClass.lean

@@ -354,7 +354,7 @@ variable [DivInvMonoid G] [Preorder G] [CovariantClass G G (· * ·) (· ≤ ·)
 @[to_additive zsmul_nonneg]
 theorem one_le_zpow {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) : 1 ≤ x ^ n := by
   lift n to ℕ using hn
-  rw [zpow_coe_nat]
+  rw [zpow_natCast]
   apply one_le_pow_of_one_le' H
 #align one_le_zpow one_le_zpow
 #align zsmul_nonneg zsmul_nonneg

Mathlib/Algebra/GroupPower/Order.lean

@@ -24,7 +24,7 @@ variable [OrderedCommGroup α] {m n : ℤ} {a b : α}
 
 @[to_additive zsmul_pos] lemma one_lt_zpow' (ha : 1 < a) (hn : 0 < n) : 1 < a ^ n := by
   obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le hn.le
-  rw [zpow_coe_nat]
+  rw [zpow_natCast]
   refine' one_lt_pow' ha ?_
   rintro rfl
   simp at hn

Mathlib/Algebra/GroupWithZero/Power.lean

@@ -58,7 +58,7 @@ variable {G₀ : Type*} [GroupWithZero G₀]
 
 theorem zero_zpow : ∀ z : ℤ, z ≠ 0 → (0 : G₀) ^ z = 0
   | (n : ℕ), h => by
-    rw [zpow_coe_nat, zero_pow]
+    rw [zpow_natCast, zero_pow]
     simpa using h
   | -[n+1], _ => by simp
 #align zero_zpow zero_zpow
@@ -70,11 +70,11 @@ theorem zero_zpow_eq (n : ℤ) : (0 : G₀) ^ n = if n = 0 then 1 else 0 := by
 #align zero_zpow_eq zero_zpow_eq
 
 theorem zpow_add_one₀ {a : G₀} (ha : a ≠ 0) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
-  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_coe_nat, pow_succ']
+  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_natCast, pow_succ']
   | -[0+1] => by erw [zpow_zero, zpow_negSucc, pow_one, inv_mul_cancel ha]
   | -[n + 1+1] => by
     rw [Int.negSucc_eq, zpow_neg, neg_add, neg_add_cancel_right, zpow_neg, ← Int.ofNat_succ,
-      zpow_coe_nat, zpow_coe_nat, pow_succ _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel ha,
+      zpow_natCast, zpow_natCast, pow_succ _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel ha,
       mul_one]
 #align zpow_add_one₀ zpow_add_one₀
 
@@ -141,7 +141,7 @@ theorem Commute.zpow_zpow_self₀ (a : G₀) (m n : ℤ) : Commute (a ^ m) (a ^
 
 theorem zpow_ne_zero_of_ne_zero {a : G₀} (ha : a ≠ 0) : ∀ z : ℤ, a ^ z ≠ 0
   | (_ : ℕ) => by
-    rw [zpow_coe_nat]
+    rw [zpow_natCast]
     exact pow_ne_zero _ ha
   | -[_+1] => by
     rw [zpow_negSucc]

Mathlib/Algebra/Lie/Weights/Chain.lean

@@ -65,7 +65,7 @@ lemma eventually_weightSpace_smul_add_eq_bot :
     simp [f]
   intro k l hkl
   replace hkl : (k : ℤ) • χ₁ = (l : ℤ) • χ₁ := by
-    simpa only [f, add_left_inj, coe_nat_zsmul] using hkl
+    simpa only [f, add_left_inj, natCast_zsmul] using hkl
   exact Nat.cast_inj.mp <| smul_left_injective ℤ hχ₁ hkl
 
 lemma exists_weightSpace_smul_add_eq_bot :
@@ -79,9 +79,9 @@ lemma exists₂_weightSpace_smul_add_eq_bot :
   obtain ⟨q, hq₀, hq⟩ := exists_weightSpace_smul_add_eq_bot M χ₁ χ₂ hχ₁
   obtain ⟨p, hp₀, hp⟩ := exists_weightSpace_smul_add_eq_bot M (-χ₁) χ₂ (neg_ne_zero.mpr hχ₁)
   refine ⟨-(p : ℤ), by simpa, q, by simpa, ?_, ?_⟩
-  · rw [neg_smul, ← smul_neg, coe_nat_zsmul]
+  · rw [neg_smul, ← smul_neg, natCast_zsmul]
     exact hp
-  · rw [coe_nat_zsmul]
+  · rw [natCast_zsmul]
     exact hq
 
 end
@@ -209,7 +209,7 @@ lemma exists_forall_mem_rootSpaceProductNegSelf_smul_add_eq_zero
     LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup _ h₁ h₂ (weightSpaceChain M α χ p q) h₃]
   simp_rw [LieSubmodule.toEndomorphism_restrict_eq_toEndomorphism,
     trace_toEndomorphism_weightSpace, Pi.add_apply, Pi.smul_apply, smul_add, ← smul_assoc,
-    Finset.sum_add_distrib, ← Finset.sum_smul, coe_nat_zsmul]
+    Finset.sum_add_distrib, ← Finset.sum_smul, natCast_zsmul]
 
 end IsCartanSubalgebra
 

Mathlib/Algebra/ModEq.lean

@@ -151,7 +151,7 @@ protected theorem of_zsmul : a ≡ b [PMOD z • p] → a ≡ b [PMOD p] := fun
 #align add_comm_group.modeq.of_zsmul AddCommGroup.ModEq.of_zsmul
 
 protected theorem of_nsmul : a ≡ b [PMOD n • p] → a ≡ b [PMOD p] := fun ⟨m, hm⟩ =>
-  ⟨m * n, by rwa [mul_smul, coe_nat_zsmul]⟩
+  ⟨m * n, by rwa [mul_smul, natCast_zsmul]⟩
 #align add_comm_group.modeq.of_nsmul AddCommGroup.ModEq.of_nsmul
 
 protected theorem zsmul : a ≡ b [PMOD p] → z • a ≡ z • b [PMOD z • p] :=

Mathlib/Algebra/Module/LinearMap/End.lean

@@ -98,7 +98,7 @@ theorem _root_.Module.End.ofNat_apply (n : ℕ) [n.AtLeastTwo] (m : M) :
 instance _root_.Module.End.ring : Ring (Module.End R N₁) :=
   { Module.End.semiring, LinearMap.addCommGroup with
     intCast := fun z ↦ z • (1 : N₁ →ₗ[R] N₁)
-    intCast_ofNat := coe_nat_zsmul _
+    intCast_ofNat := natCast_zsmul _
     intCast_negSucc := negSucc_zsmul _ }
 #align module.End.ring Module.End.ring
 

Mathlib/Algebra/Module/Torsion.lean

@@ -866,7 +866,7 @@ theorem isTorsion_iff_isTorsion_int [AddCommGroup M] :
   · obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero
     exact
       ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt <| Int.coe_nat_pos.mpr h0⟩,
-        (coe_nat_zsmul _ _).trans hn⟩
+        (natCast_zsmul _ _).trans hn⟩
   · rw [isOfFinAddOrder_iff_nsmul_eq_zero]
     obtain ⟨n, hn⟩ := @h x
     exact ⟨_, Int.natAbs_pos.2 (nonZeroDivisors.coe_ne_zero n), natAbs_nsmul_eq_zero.2 hn⟩

Mathlib/Algebra/Order/Archimedean.lean

@@ -71,7 +71,7 @@ theorem existsUnique_zsmul_near_of_pos {a : α} (ha : 0 < a) (g : α) :
   have h_bdd : ∀ n ∈ s, n ≤ (k : ℤ) := by
     intro n hn
     apply (zsmul_le_zsmul_iff ha).mp
-    rw [← coe_nat_zsmul] at hk
+    rw [← natCast_zsmul] at hk
     exact le_trans hn hk
   obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne
   have hm'' : g < (m + 1) • a := by
@@ -217,14 +217,14 @@ theorem exists_mem_Ico_zpow (hx : 0 < x) (hy : 1 < y) : ∃ n : ℤ, x ∈ Ico (
         ⟨-N,
           le_of_lt
             (by
-              rw [zpow_neg y ↑N, zpow_coe_nat]
+              rw [zpow_neg y ↑N, zpow_natCast]
               exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩
       let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
       have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b :=
         ⟨M, fun m hm =>
           le_of_not_lt fun hlt =>
             not_lt_of_ge (zpow_le_of_le hy.le hlt.le)
-              (lt_of_le_of_lt hm (by rwa [← zpow_coe_nat] at hM))⟩
+              (lt_of_le_of_lt hm (by rwa [← zpow_natCast] at hM))⟩
       let ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
       ⟨n, hn₁, lt_of_not_ge fun hge => not_le_of_gt (Int.lt_succ _) (hn₂ _ hge)⟩
 #align exists_mem_Ico_zpow exists_mem_Ico_zpow