chore(Data/Int): Rename coe_nat to natCast (#11637)

Reduce the diff of #11499

## Renames

All in the `Int` namespace:
* `ofNat_eq_cast` → `ofNat_eq_natCast`
* `cast_eq_cast_iff_Nat` → `natCast_inj`
* `natCast_eq_ofNat` → `ofNat_eq_natCast`
* `coe_nat_sub` → `natCast_sub`
* `coe_nat_nonneg` → `natCast_nonneg`
* `sign_coe_add_one` → `sign_natCast_add_one`
* `nat_succ_eq_int_succ` → `natCast_succ`
* `succ_neg_nat_succ` → `succ_neg_natCast_succ`
* `coe_pred_of_pos` → `natCast_pred_of_pos`
* `coe_nat_div` → `natCast_div`
* `coe_nat_ediv` → `natCast_ediv`
* `sign_coe_nat_of_nonzero` → `sign_natCast_of_ne_zero`
* `toNat_coe_nat` → `toNat_natCast`
* `toNat_coe_nat_add_one` → `toNat_natCast_add_one`
* `coe_nat_dvd` → `natCast_dvd_natCast`
* `coe_nat_dvd_left` → `natCast_dvd`
* `coe_nat_dvd_right` → `dvd_natCast`
* `le_coe_nat_sub` → `le_natCast_sub`
* `succ_coe_nat_pos` → `succ_natCast_pos`
* `coe_nat_modEq_iff` → `natCast_modEq_iff`
* `coe_natAbs` → `natCast_natAbs`
* `coe_nat_eq_zero` → `natCast_eq_zero`
* `coe_nat_ne_zero` → `natCast_ne_zero`
* `coe_nat_ne_zero_iff_pos` → `natCast_ne_zero_iff_pos`
* `abs_coe_nat` → `abs_natCast`
* `coe_nat_nonpos_iff` → `natCast_nonpos_iff`

Also rename `Nat.coe_nat_dvd` to `Nat.cast_dvd_cast`

Archive/Imo/Imo1988Q6.lean

@@ -207,7 +207,7 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
     clear hk a b
   · -- We will now show that the fibers of the solution set are described by a quadratic equation.
     intro x y
-    rw [← Int.coe_nat_inj', ← sub_eq_zero]
+    rw [← Int.natCast_inj, ← sub_eq_zero]
     apply eq_iff_eq_cancel_right.2
     simp; ring
   · -- Show that the solution set is symmetric in a and b.
@@ -265,7 +265,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
     clear hk a b
   · -- We will now show that the fibers of the solution set are described by a quadratic equation.
     intro x y
-    rw [← Int.coe_nat_inj', ← sub_eq_zero]
+    rw [← Int.natCast_inj, ← sub_eq_zero]
     apply eq_iff_eq_cancel_right.2
     simp; ring
   · -- Show that the solution set is symmetric in a and b.

Archive/Imo/Imo2005Q4.lean

@@ -66,7 +66,7 @@ theorem imo2005_q4 {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → IsCoprime
   have hp : Nat.Prime p := Nat.minFac_prime hk'
   replace h : ∀ n, 1 ≤ n → ¬(p : ℤ) ∣ a n := fun n hn ↦ by
     have : IsCoprime (a n) p :=
-      .of_isCoprime_of_dvd_right (h n hn) (Int.coe_nat_dvd.mpr k.minFac_dvd)
+      .of_isCoprime_of_dvd_right (h n hn) (Int.natCast_dvd_natCast.mpr k.minFac_dvd)
     rwa [isCoprime_comm,(Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd] at this
   -- For `p = 2` and `p = 3`, take `n = 1` and `n = 2`, respectively
   by_cases hp2 : p = 2

Archive/Imo/Imo2008Q3.lean

@@ -41,8 +41,8 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   let m := ZMod.valMinAbs y
   let n := Int.natAbs m
   have hnat₁ : p ∣ n ^ 2 + 1 := by
-    refine' Int.coe_nat_dvd.mp _
-    simp only [n, Int.natAbs_sq, Int.coe_nat_pow, Int.ofNat_succ, Int.coe_nat_dvd.mp]
+    refine' Int.natCast_dvd_natCast.mp _
+    simp only [n, Int.natAbs_sq, Int.coe_nat_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
     refine' (ZMod.int_cast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp _
     simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
     rw [pow_two, ← hy]; exact add_left_neg 1

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -86,20 +86,20 @@ theorem irreducible_Phi (p : ℕ) (hp : p.Prime) (hpa : p ∣ a) (hpb : p ∣ b)
     Irreducible (Φ ℚ a b) := by
   rw [← map_Phi a b (Int.castRingHom ℚ), ← IsPrimitive.Int.irreducible_iff_irreducible_map_cast]
   apply irreducible_of_eisenstein_criterion
-  · rwa [span_singleton_prime (Int.coe_nat_ne_zero.mpr hp.ne_zero), Int.prime_iff_natAbs_prime]
+  · rwa [span_singleton_prime (Int.natCast_ne_zero.mpr hp.ne_zero), Int.prime_iff_natAbs_prime]
   · rw [leadingCoeff_Phi, mem_span_singleton]
     exact mod_cast mt Nat.dvd_one.mp hp.ne_one
   · intro n hn
     rw [mem_span_singleton]
     rw [degree_Phi] at hn; norm_cast at hn
     interval_cases hn : n <;>
-    simp (config := {decide := true}) only [Φ, coeff_X_pow, coeff_C, Int.coe_nat_dvd.mpr, hpb,
-      if_true, coeff_C_mul, if_false, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero, coeff_sub,
-      add_zero, zero_sub, dvd_neg, neg_zero, dvd_mul_of_dvd_left]
+    simp (config := {decide := true}) only [Φ, coeff_X_pow, coeff_C, Int.natCast_dvd_natCast.mpr,
+      hpb, if_true, coeff_C_mul, if_false, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero,
+      coeff_sub, add_zero, zero_sub, dvd_neg, neg_zero, dvd_mul_of_dvd_left]
   · simp only [degree_Phi, ← WithBot.coe_zero, WithBot.coe_lt_coe, Nat.succ_pos']
     decide
   · rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton]
-    exact mt Int.coe_nat_dvd.mp hp2b
+    exact mt Int.natCast_dvd_natCast.mp hp2b
   all_goals exact Monic.isPrimitive (monic_Phi a b)
 #align abel_ruffini.irreducible_Phi AbelRuffini.irreducible_Phi
 

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.coe_nat_dvd]
+    rw [Int.cast_ofNat, 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.coe_nat_dvd]
+    rw [Int.cast_ofNat, 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/CharAndCard.lean

@@ -60,7 +60,7 @@ theorem prime_dvd_char_iff_dvd_card {R : Type*} [CommRing R] [Fintype R] (p : 
   refine'
     ⟨fun h =>
       h.trans <|
-        Int.coe_nat_dvd.mp <|
+        Int.natCast_dvd_natCast.mp <|
           (CharP.int_cast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <|
             mod_cast CharP.cast_card_eq_zero R,
       fun h => _⟩

Mathlib/Algebra/CharZero/Quotient.lean

@@ -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 [← natCast_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.natCast_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
@@ -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.coe_nat_ne_zero.mpr hz), Int.cast_ofNat]
+    zmultiples_zsmul_eq_zsmul_iff (Int.natCast_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/ModEq.lean

@@ -328,7 +328,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.coe_nat_modEq_iff, ← modEq_iff_int_modEq, ← @intCast_modEq_intCast α,
+  simp_rw [← Int.natCast_modEq_iff, ← modEq_iff_int_modEq, ← @intCast_modEq_intCast α,
     Int.cast_ofNat]
 #align add_comm_group.nat_cast_modeq_nat_cast AddCommGroup.natCast_modEq_natCast
 

Mathlib/Algebra/Order/Field/Power.lean

@@ -56,7 +56,7 @@ theorem Nat.zpow_ne_zero_of_pos {a : ℕ} (h : 0 < a) (n : ℤ) : (a : α) ^ n 
 #align nat.zpow_ne_zero_of_pos Nat.zpow_ne_zero_of_pos
 
 theorem one_lt_zpow (ha : 1 < a) : ∀ n : ℤ, 0 < n → 1 < a ^ n
-  | (n : ℕ), h => (zpow_natCast _ _).symm.subst (one_lt_pow ha <| Int.coe_nat_ne_zero.mp h.ne')
+  | (n : ℕ), h => (zpow_natCast _ _).symm.subst (one_lt_pow ha <| Int.natCast_ne_zero.mp h.ne')
   | -[_+1], h => ((Int.negSucc_not_pos _).mp h).elim
 #align one_lt_zpow one_lt_zpow
 

Mathlib/Algebra/Order/Floor.lean

@@ -1151,8 +1151,8 @@ 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, ← coe_nat_mod, cast_ofNat, fract_div_natCast_eq_div_natCast_mod]
-    · rw [Right.nonneg_neg_iff, coe_nat_nonpos_iff] at hl
+    · rw [cast_ofNat, ← natCast_mod, cast_ofNat, 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
   · exact this (ofNat_nonneg m₀)

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -1925,16 +1925,16 @@ theorem norm_eq_abs (n : ℤ) : ‖n‖ = |(n : ℝ)| :=
 theorem norm_coe_nat (n : ℕ) : ‖(n : ℤ)‖ = n := by simp [Int.norm_eq_abs]
 #align int.norm_coe_nat Int.norm_coe_nat
 
-theorem _root_.NNReal.coe_natAbs (n : ℤ) : (n.natAbs : ℝ≥0) = ‖n‖₊ :=
+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 : ℝ)| := by simp only [Int.coe_natAbs, Int.cast_abs]
+      _ = |(n : ℝ)| := by simp only [Int.natCast_natAbs, Int.cast_abs]
       _ = ‖n‖ := (norm_eq_abs n).symm
-#align nnreal.coe_nat_abs NNReal.coe_natAbs
+#align nnreal.coe_nat_abs NNReal.natCast_natAbs
 
 theorem abs_le_floor_nnreal_iff (z : ℤ) (c : ℝ≥0) : |z| ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c := by
-  rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff (zero_le c), NNReal.coe_natAbs z]
+  rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff (zero_le c), NNReal.natCast_natAbs z]
 #align int.abs_le_floor_nnreal_iff Int.abs_le_floor_nnreal_iff
 
 end Int

Mathlib/Analysis/NormedSpace/Int.lean

@@ -39,7 +39,7 @@ theorem nnnorm_coe_nat (n : ℕ) : ‖(n : ℤ)‖₊ = n :=
 
 @[simp]
 theorem toNat_add_toNat_neg_eq_nnnorm (n : ℤ) : ↑n.toNat + ↑(-n).toNat = ‖n‖₊ := by
-  rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.coe_natAbs]
+  rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.natCast_natAbs]
 #align int.to_nat_add_to_nat_neg_eq_nnnorm Int.toNat_add_toNat_neg_eq_nnnorm
 
 @[simp]

Mathlib/Analysis/SpecialFunctions/Integrals.lean

@@ -408,7 +408,7 @@ theorem integral_zpow {n : ℤ} (h : 0 ≤ n ∨ n ≠ -1 ∧ (0 : ℝ) ∉ [[a,
 
 @[simp]
 theorem integral_pow : ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) := by
-  simpa only [← Int.ofNat_succ, zpow_natCast] using integral_zpow (Or.inl (Int.coe_nat_nonneg n))
+  simpa only [← Int.ofNat_succ, zpow_natCast] using integral_zpow (Or.inl n.cast_nonneg)
 #align integral_pow integral_pow
 
 /-- Integral of `|x - a| ^ n` over `Ι a b`. This integral appears in the proof of the

Mathlib/Data/Int/Bitwise.lean

@@ -67,7 +67,7 @@ theorem bodd_neg (n : ℤ) : bodd (-n) = bodd n := by
     change (!Nat.bodd n) = !(bodd n)
     rw [bodd_coe]
 -- Porting note: Heavily refactored proof, used to work all with `simp`:
--- `cases n <;> simp [Neg.neg, Int.coe_nat_eq, Int.neg, bodd, -of_nat_eq_coe]`
+-- `cases n <;> simp [Neg.neg, Int.natCast_eq_ofNat, Int.neg, bodd, -of_nat_eq_coe]`
 #align int.bodd_neg Int.bodd_neg
 
 @[simp]

Mathlib/Data/Int/CardIntervalMod.lean

@@ -83,16 +83,16 @@ lemma Ico_filter_modEq_cast {v : ℕ} : ((Ico a b).filter (· ≡ v [MOD r])).ma
   ext x
   simp only [mem_map, mem_filter, mem_Ico, castEmbedding_apply]
   constructor
-  · simp_rw [forall_exists_index, ← coe_nat_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h
-  · intro h; lift x to ℕ using (by linarith); exact ⟨x, by simp_all [coe_nat_modEq_iff]⟩
+  · simp_rw [forall_exists_index, ← natCast_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h
+  · intro h; lift x to ℕ using (by linarith); exact ⟨x, by simp_all [natCast_modEq_iff]⟩
 
 lemma Ioc_filter_modEq_cast {v : ℕ} : ((Ioc a b).filter (· ≡ v [MOD r])).map castEmbedding =
     (Ioc ↑a ↑b).filter (· ≡ v [ZMOD r]) := by
   ext x
   simp only [mem_map, mem_filter, mem_Ioc, castEmbedding_apply]
   constructor
-  · simp_rw [forall_exists_index, ← coe_nat_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h
-  · intro h; lift x to ℕ using (by linarith); exact ⟨x, by simp_all [coe_nat_modEq_iff]⟩
+  · simp_rw [forall_exists_index, ← natCast_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h
+  · intro h; lift x to ℕ using (by linarith); exact ⟨x, by simp_all [natCast_modEq_iff]⟩
 
 /-- There are `⌈(b - v) / r⌉ - ⌈(a - v) / r⌉` numbers congruent to `v` mod `r` in `[a, b)`,
 if `a ≤ b`. `Nat` version of `Int.Ico_filter_modEq_card`. -/

Mathlib/Data/Int/Cast/Basic.lean

@@ -61,7 +61,8 @@ theorem cast_zero : ((0 : ℤ) : R) = 0 :=
 #align int.cast_zero Int.cast_zeroₓ
 -- type had `HasLiftT`
 
-@[simp high, nolint simpNF, norm_cast] -- this lemma competes with `Int.ofNat_eq_cast` to come later
+-- This lemma competes with `Int.ofNat_eq_natCast` to come later
+@[simp high, nolint simpNF, norm_cast]
 theorem cast_ofNat (n : ℕ) : ((n : ℤ) : R) = n :=
   AddGroupWithOne.intCast_ofNat _
 #align int.cast_coe_nat Int.cast_ofNatₓ

Mathlib/Data/Int/Cast/Lemmas.lean

@@ -46,7 +46,7 @@ theorem coe_nat_succ_pos (n : ℕ) : 0 < (n.succ : ℤ) :=
 #align int.coe_nat_succ_pos Int.coe_nat_succ_pos
 
 lemma toNat_lt' {a : ℤ} {b : ℕ} (hb : b ≠ 0) : a.toNat < b ↔ a < b := by
-  rw [← toNat_lt_toNat, toNat_coe_nat]; exact coe_nat_pos.2 hb.bot_lt
+  rw [← toNat_lt_toNat, toNat_natCast]; exact coe_nat_pos.2 hb.bot_lt
 #align int.to_nat_lt Int.toNat_lt'
 
 lemma natMod_lt {a : ℤ} {b : ℕ} (hb : b ≠ 0) : a.natMod b < b :=

Mathlib/Data/Int/Defs.lean

@@ -24,14 +24,19 @@ attribute [simp] natAbs_pos
 
 instance instNontrivialInt : Nontrivial ℤ := ⟨⟨0, 1, Int.zero_ne_one⟩⟩
 
-@[simp] lemma ofNat_eq_cast : Int.ofNat n = n := rfl
+@[simp] lemma ofNat_eq_natCast : Int.ofNat n = n := rfl
 
-@[norm_cast] lemma cast_eq_cast_iff_Nat (m n : ℕ) : (m : ℤ) = (n : ℤ) ↔ m = n := ofNat_inj
+-- 2024-03-24
+@[deprecated ofNat_eq_natCast] protected lemma natCast_eq_ofNat (n : ℕ) : ↑n = Int.ofNat n := rfl
+#align int.coe_nat_eq Int.natCast_eq_ofNat
+
+@[norm_cast] lemma natCast_inj : (m : ℤ) = (n : ℤ) ↔ m = n := ofNat_inj
+#align int.coe_nat_inj' Int.natCast_inj
 
 @[simp, norm_cast] lemma natAbs_cast (n : ℕ) : natAbs ↑n = n := rfl
 
 @[norm_cast]
-protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := ofNat_sub
+protected lemma natCast_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := ofNat_sub
 
 #align int.neg_succ_not_nonneg Int.negSucc_not_nonneg
 #align int.neg_succ_not_pos Int.negSucc_not_pos
@@ -43,17 +48,14 @@ protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m
 #align int.coe_nat_le Int.ofNat_le
 #align int.coe_nat_lt Int.ofNat_lt
 
-lemma coe_nat_inj' : (↑m : ℤ) = ↑n ↔ m = n := Int.ofNat_inj
-#align int.coe_nat_inj' Int.coe_nat_inj'
-
-lemma coe_nat_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := ofNat_le.2 (Nat.zero_le _)
-#align int.coe_nat_nonneg Int.coe_nat_nonneg
+lemma natCast_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := ofNat_le.2 (Nat.zero_le _)
+#align int.coe_nat_nonneg Int.natCast_nonneg
 
 #align int.neg_of_nat_ne_zero Int.negSucc_ne_zero
 #align int.zero_ne_neg_of_nat Int.zero_ne_negSucc
 
-@[simp] lemma sign_coe_add_one (n : ℕ) : sign (n + 1) = 1 := rfl
-#align int.sign_coe_add_one Int.sign_coe_add_one
+@[simp] lemma sign_natCast_add_one (n : ℕ) : sign (n + 1) = 1 := rfl
+#align int.sign_coe_add_one Int.sign_natCast_add_one
 
 #align int.sign_neg_succ_of_nat Int.sign_negSucc
 
@@ -85,8 +87,8 @@ def succ (a : ℤ) := a + 1
 def pred (a : ℤ) := a - 1
 #align int.pred Int.pred
 
-lemma nat_succ_eq_int_succ (n : ℕ) : (Nat.succ n : ℤ) = Int.succ n := rfl
-#align int.nat_succ_eq_int_succ Int.nat_succ_eq_int_succ
+lemma natCast_succ (n : ℕ) : (Nat.succ n : ℤ) = Int.succ n := rfl
+#align int.nat_succ_eq_int_succ Int.natCast_succ
 
 lemma pred_succ (a : ℤ) : pred (succ a) = a := Int.add_sub_cancel _ _
 #align int.pred_succ Int.pred_succ
@@ -113,12 +115,12 @@ lemma pred_nat_succ (n : ℕ) : pred (Nat.succ n) = n := pred_succ n
 lemma neg_nat_succ (n : ℕ) : -(Nat.succ n : ℤ) = pred (-n) := neg_succ n
 #align int.neg_nat_succ Int.neg_nat_succ
 
-lemma succ_neg_nat_succ (n : ℕ) : succ (-Nat.succ n) = -n := succ_neg_succ n
-#align int.succ_neg_nat_succ Int.succ_neg_nat_succ
+lemma succ_neg_natCast_succ (n : ℕ) : succ (-Nat.succ n) = -n := succ_neg_succ n
+#align int.succ_neg_nat_succ Int.succ_neg_natCast_succ
 
-@[norm_cast] lemma coe_pred_of_pos {n : ℕ} (h : 0 < n) : ((n - 1 : ℕ) : ℤ) = (n : ℤ) - 1 := by
+@[norm_cast] lemma natCast_pred_of_pos {n : ℕ} (h : 0 < n) : ((n - 1 : ℕ) : ℤ) = (n : ℤ) - 1 := by
   cases n; cases h; simp [ofNat_succ]
-#align int.coe_pred_of_pos Int.coe_pred_of_pos
+#align int.coe_pred_of_pos Int.natCast_pred_of_pos
 
 @[elab_as_elim] protected lemma induction_on {p : ℤ → Prop} (i : ℤ)
     (hz : p 0) (hp : ∀ i : ℕ, p i → p (i + 1)) (hn : ∀ i : ℕ, p (-i) → p (-i - 1)) : p i := by
@@ -167,10 +169,10 @@ lemma natAbs_ne_zero_of_ne_zero : ∀ {a : ℤ}, a ≠ 0 → natAbs a ≠ 0 := n
 
 #align int.of_nat_div Int.ofNat_div
 
-@[simp, norm_cast] lemma coe_nat_div (m n : ℕ) : ((m / n : ℕ) : ℤ) = m / n := rfl
-#align int.coe_nat_div Int.coe_nat_div
+@[simp, norm_cast] lemma natCast_div (m n : ℕ) : ((m / n : ℕ) : ℤ) = m / n := rfl
+#align int.coe_nat_div Int.natCast_div
 
-lemma coe_nat_ediv (m n : ℕ) : ((m / n : ℕ) : ℤ) = ediv m n := rfl
+lemma natCast_ediv (m n : ℕ) : ((m / n : ℕ) : ℤ) = ediv m n := rfl
 
 #align int.neg_succ_of_nat_div Int.negSucc_ediv
 
@@ -191,8 +193,8 @@ lemma ediv_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : 0 < b) : ediv a b = -((-
 
 #align int.of_nat_mod Int.ofNat_mod_ofNat
 
-@[simp, norm_cast] lemma coe_nat_mod (m n : ℕ) : (↑(m % n) : ℤ) = ↑m % ↑n := rfl
-#align int.coe_nat_mod Int.coe_nat_mod
+@[simp, norm_cast] lemma natCast_mod (m n : ℕ) : (↑(m % n) : ℤ) = ↑m % ↑n := rfl
+#align int.coe_nat_mod Int.natCast_mod
 
 #align int.neg_succ_of_nat_mod Int.negSucc_emod
 #align int.mod_neg Int.mod_negₓ -- int div alignment
@@ -217,8 +219,8 @@ lemma ediv_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : 0 < b) : ediv a b = -((-
 #align int.nat_abs_sign Int.natAbs_sign
 #align int.nat_abs_sign_of_nonzero Int.natAbs_sign_of_nonzero
 
-lemma sign_coe_nat_of_nonzero {n : ℕ} (hn : n ≠ 0) : Int.sign n = 1 := sign_ofNat_of_nonzero hn
-#align int.sign_coe_nat_of_nonzero Int.sign_coe_nat_of_nonzero
+lemma sign_natCast_of_ne_zero (hn : n ≠ 0) : Int.sign n = 1 := sign_ofNat_of_nonzero hn
+#align int.sign_coe_nat_of_nonzero Int.sign_natCast_of_ne_zero
 
 #align int.div_sign Int.div_sign -- int div alignment
 #align int.of_nat_add_neg_succ_of_nat_of_lt Int.ofNat_add_negSucc_of_lt
@@ -231,11 +233,11 @@ lemma sign_coe_nat_of_nonzero {n : ℕ} (hn : n ≠ 0) : Int.sign n = 1 := sign_
 #align int.to_nat_one Int.toNat_one
 #align int.to_nat_of_nonneg Int.toNat_of_nonneg
 
-@[simp] lemma toNat_coe_nat (n : ℕ) : toNat ↑n = n := rfl
-#align int.to_nat_coe_nat Int.toNat_coe_nat
+@[simp] lemma toNat_natCast (n : ℕ) : toNat ↑n = n := rfl
+#align int.to_nat_coe_nat Int.toNat_natCast
 
-@[simp] lemma toNat_coe_nat_add_one {n : ℕ} : ((n : ℤ) + 1).toNat = n + 1 := rfl
-#align int.to_nat_coe_nat_add_one Int.toNat_coe_nat_add_one
+@[simp] lemma toNat_natCast_add_one {n : ℕ} : ((n : ℤ) + 1).toNat = n + 1 := rfl
+#align int.to_nat_coe_nat_add_one Int.toNat_natCast_add_one
 
 #align int.le_to_nat Int.self_le_toNat
 #align int.le_to_nat_iff Int.le_toNat
@@ -249,3 +251,18 @@ lemma sign_coe_nat_of_nonzero {n : ℕ} (hn : n ≠ 0) : Int.sign n = 1 := sign_
 
 -- Porting note: this was added in an ad hoc port for use in `Tactic/NormNum/Basic`
 @[simp] lemma pow_eq (m : ℤ) (n : ℕ) : m.pow n = m ^ n := rfl
+
+-- 2024-04-02
+@[deprecated] alias ofNat_eq_cast := ofNat_eq_natCast
+@[deprecated] alias cast_eq_cast_iff_Nat := natCast_inj
+@[deprecated] alias coe_nat_sub := Int.natCast_sub
+@[deprecated] alias coe_nat_nonneg := natCast_nonneg
+@[deprecated] alias sign_coe_add_one := sign_natCast_add_one
+@[deprecated] alias nat_succ_eq_int_succ := natCast_succ
+@[deprecated] alias succ_neg_nat_succ := succ_neg_natCast_succ
+@[deprecated] alias coe_pred_of_pos := natCast_pred_of_pos
+@[deprecated] alias coe_nat_div := natCast_div
+@[deprecated] alias coe_nat_ediv := natCast_ediv
+@[deprecated] alias sign_coe_nat_of_nonzero := sign_natCast_of_ne_zero
+@[deprecated] alias toNat_coe_nat := toNat_natCast
+@[deprecated] alias toNat_coe_nat_add_one := toNat_natCast_add_one