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`

Author: YaelDillies

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₀)