chore: Rename nat_cast/int_cast/rat_cast to natCast/intCast…

…/`ratCast` (#11486)

Now that I am defining `NNRat.cast`, I want a definitive answer to this naming issue. Plenty of lemmas in mathlib already use `natCast`/`intCast`/`ratCast` over `nat_cast`/`int_cast`/`rat_cast`, and this matches with the general expectation that underscore-separated name parts correspond to a single declaration.

Archive/Imo/Imo2006Q5.lean

@@ -161,7 +161,7 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
         rw [natDegree_add_eq_left_of_natDegree_lt]
         simpa using hP
       rwa [natDegree_sub_eq_left_of_natDegree_lt]
-      rw [h₁, natDegree_int_cast]
+      rw [h₁, natDegree_intCast]
       exact zero_lt_one.trans hP
     have hPab' : P + (X : ℤ[X]) - a - b ≠ 0 := by
       intro h
@@ -178,7 +178,7 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
       replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
       rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
       simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def,
-        eval_sub, eval_add, eval_X, eval_C, eval_int_cast, Int.cast_id, zero_add]
+        eval_sub, eval_add, eval_X, eval_C, eval_intCast, Int.cast_id, zero_add]
       -- An auxiliary lemma proved earlier implies we only need to show |t - a| = |u - b| and
       -- |t - b| = |u - a|. We prove this by establishing that each side of either equation divides
       -- the other.

Archive/Imo/Imo2008Q3.lean

@@ -43,7 +43,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   have hnat₁ : p ∣ n ^ 2 + 1 := by
     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 _
+    refine' (ZMod.intCast_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
   have hnat₂ : n ≤ p / 2 := ZMod.natAbs_valMinAbs_le y

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -240,7 +240,7 @@ variable [Nonempty V]
 theorem false_of_three_le_degree (hd : G.IsRegularOfDegree d) (h : 3 ≤ d) : False := by
   -- get a prime factor of d - 1
   let p : ℕ := (d - 1).minFac
-  have p_dvd_d_pred := (ZMod.nat_cast_zmod_eq_zero_iff_dvd _ _).mpr (d - 1).minFac_dvd
+  have p_dvd_d_pred := (ZMod.natCast_zmod_eq_zero_iff_dvd _ _).mpr (d - 1).minFac_dvd
   have dpos : 1 ≤ d := by linarith
   have d_cast : ↑(d - 1) = (d : ℤ) - 1 := by norm_cast
   haveI : Fact p.Prime := ⟨Nat.minFac_prime (by linarith)⟩
@@ -260,7 +260,7 @@ theorem false_of_three_le_degree (hd : G.IsRegularOfDegree d) (h : 3 ≤ d) : Fa
   dsimp only [Fintype.card] at Vmod
   simp only [Matrix.trace, Matrix.diag, mul_one, nsmul_eq_mul, LinearMap.coe_mk, sum_const,
     of_apply, Ne]
-  rw [Vmod, ← Nat.cast_one (R := ZMod (Nat.minFac (d - 1))), ZMod.nat_cast_zmod_eq_zero_iff_dvd,
+  rw [Vmod, ← Nat.cast_one (R := ZMod (Nat.minFac (d - 1))), ZMod.natCast_zmod_eq_zero_iff_dvd,
     Nat.dvd_one, Nat.minFac_eq_one_iff]
   linarith
 #align theorems_100.friendship.false_of_three_le_degree Theorems100.Friendship.false_of_three_le_degree

Counterexamples/MapFloor.lean

@@ -97,14 +97,14 @@ instance : FloorRing ℤ[ε] :=
       · rintro ⟨_ | n, hn⟩
         · refine' (sub_one_lt _).trans _
           simp at hn
-          rwa [int_cast_coeff_zero] at hn
+          rwa [intCast_coeff_zero] at hn
         · dsimp at hn
           simp [hn.1 _ n.zero_lt_succ]
-          rw [int_cast_coeff_zero]; simp
+          rw [intCast_coeff_zero]; simp
       · exact fun h' => cast_lt.1 ((not_lt.1 h).trans_lt h')
     · split_ifs with h
       · exact fun h' => h.trans_le (cast_le.2 <| sub_one_lt_iff.1 h')
-      · exact fun h' => ⟨0, by simp; rwa [int_cast_coeff_zero]⟩
+      · exact fun h' => ⟨0, by simp; rwa [intCast_coeff_zero]⟩
 
 /-- The ordered ring homomorphisms from `ℤ[ε]` to `ℤ` that "forgets" the `ε`s. -/
 def forgetEpsilons : ℤ[ε] →+*o ℤ where
@@ -131,8 +131,8 @@ theorem forgetEpsilons_floor_lt (n : ℤ) :
     forgetEpsilons ⌊(n - ↑ε : ℤ[ε])⌋ < ⌊forgetEpsilons (n - ↑ε)⌋ := by
   suffices ⌊(n - ↑ε : ℤ[ε])⌋ = n - 1 by simp [this]
   have : (0 : ℤ[ε]) < ε := ⟨1, by simp⟩
-  exact (if_neg <| by rw [coeff_sub, int_cast_coeff_zero]; simp [this]).trans (by
-    rw [coeff_sub, int_cast_coeff_zero]; simp)
+  exact (if_neg <| by rw [coeff_sub, intCast_coeff_zero]; simp [this]).trans (by
+    rw [coeff_sub, intCast_coeff_zero]; simp)
 #align counterexample.int_with_epsilon.forget_epsilons_floor_lt Counterexample.IntWithEpsilon.forgetEpsilons_floor_lt
 
 /-- The ceil of `n + ε` is `n + 1` but its image under `forgetEpsilons` is `n`, whose ceil is

Mathlib/Algebra/CharP/Basic.lean

@@ -140,7 +140,7 @@ theorem CharP.addOrderOf_one (R) [Semiring R] : CharP R (addOrderOf (1 : R)) :=
   ⟨fun n => by rw [← Nat.smul_one_eq_coe, addOrderOf_dvd_iff_nsmul_eq_zero]⟩
 #align char_p.add_order_of_one CharP.addOrderOf_one
 
-theorem CharP.int_cast_eq_zero_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a : ℤ) :
+theorem CharP.intCast_eq_zero_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a : ℤ) :
     (a : R) = 0 ↔ (p : ℤ) ∣ a := by
   rcases lt_trichotomy a 0 with (h | rfl | h)
   · rw [← neg_eq_zero, ← Int.cast_neg, ← dvd_neg]
@@ -149,11 +149,11 @@ theorem CharP.int_cast_eq_zero_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a
   · simp only [Int.cast_zero, eq_self_iff_true, dvd_zero]
   · lift a to ℕ using le_of_lt h with b
     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
+#align char_p.int_cast_eq_zero_iff CharP.intCast_eq_zero_iff
 
 theorem CharP.intCast_eq_intCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℤ} :
     (a : R) = b ↔ a ≡ b [ZMOD p] := by
-  rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
+  rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.intCast_eq_zero_iff R p, Int.modEq_iff_dvd]
 #align char_p.int_cast_eq_int_cast CharP.intCast_eq_intCast
 
 theorem CharP.natCast_eq_natCast' [AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ}

Mathlib/Algebra/CharP/CharAndCard.lean

@@ -32,7 +32,7 @@ theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero (R : Type*) [CommRing R] (p
       rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
       nth_rw 1 [← mul_one (ringChar R)] at hq
       exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
-    have h₄ := mt (CharP.int_cast_eq_zero_iff R (ringChar R) q).mp
+    have h₄ := mt (CharP.intCast_eq_zero_iff R (ringChar R) q).mp
     apply_fun ((↑) : ℕ → R) at hq
     apply_fun (· * ·) a at hq
     rw [Nat.cast_mul, hch, mul_zero, ← mul_assoc, ha, one_mul] at hq
@@ -61,7 +61,7 @@ theorem prime_dvd_char_iff_dvd_card {R : Type*} [CommRing R] [Fintype R] (p : 
     ⟨fun h =>
       h.trans <|
         Int.natCast_dvd_natCast.mp <|
-          (CharP.int_cast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <|
+          (CharP.intCast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <|
             mod_cast CharP.cast_card_eq_zero R,
       fun h => _⟩
   by_contra h₀

Mathlib/Algebra/CharP/ExpChar.lean

@@ -397,9 +397,9 @@ theorem frobenius_add : frobenius R p (x + y) = frobenius R p x + frobenius R p
   (frobenius R p).map_add x y
 #align frobenius_add frobenius_add
 
-theorem frobenius_nat_cast (n : ℕ) : frobenius R p n = n :=
+theorem frobenius_natCast (n : ℕ) : frobenius R p n = n :=
   map_natCast (frobenius R p) n
-#align frobenius_nat_cast frobenius_nat_cast
+#align frobenius_nat_cast frobenius_natCast
 
 open BigOperators
 

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -63,13 +63,13 @@ instance CharZero.NeZero.two : NeZero (2 : M) :=
 
 namespace Function
 
-lemma support_nat_cast (hn : n ≠ 0) : support (n : α → M) = univ :=
+lemma support_natCast (hn : n ≠ 0) : support (n : α → M) = univ :=
   support_const <| Nat.cast_ne_zero.2 hn
-#align function.support_nat_cast Function.support_nat_cast
+#align function.support_nat_cast Function.support_natCast
 
-lemma mulSupport_nat_cast (hn : n ≠ 1) : mulSupport (n : α → M) = univ :=
+lemma mulSupport_natCast (hn : n ≠ 1) : mulSupport (n : α → M) = univ :=
   mulSupport_const <| Nat.cast_ne_one.2 hn
-#align function.mul_support_nat_cast Function.mulSupport_nat_cast
+#align function.mul_support_nat_cast Function.mulSupport_natCast
 
 end Function
 end AddMonoidWithOne

Mathlib/Algebra/DirectSum/Internal.lean

@@ -59,23 +59,23 @@ theorem SetLike.algebraMap_mem_graded [Zero ι] [CommSemiring S] [Semiring R] [A
   exact (A 0).smul_mem s <| SetLike.one_mem_graded _
 #align set_like.algebra_map_mem_graded SetLike.algebraMap_mem_graded
 
-theorem SetLike.nat_cast_mem_graded [Zero ι] [AddMonoidWithOne R] [SetLike σ R]
+theorem SetLike.natCast_mem_graded [Zero ι] [AddMonoidWithOne R] [SetLike σ R]
     [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedOne A] (n : ℕ) : (n : R) ∈ A 0 := by
   induction' n with _ n_ih
   · rw [Nat.cast_zero]
     exact zero_mem (A 0)
   · rw [Nat.cast_succ]
     exact add_mem n_ih (SetLike.one_mem_graded _)
-#align set_like.nat_cast_mem_graded SetLike.nat_cast_mem_graded
+#align set_like.nat_cast_mem_graded SetLike.natCast_mem_graded
 
-theorem SetLike.int_cast_mem_graded [Zero ι] [AddGroupWithOne R] [SetLike σ R]
+theorem SetLike.intCast_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_natCast]
-    exact SetLike.nat_cast_mem_graded _ _
+    exact SetLike.natCast_mem_graded _ _
   · rw [Int.cast_negSucc]
-    exact neg_mem (SetLike.nat_cast_mem_graded _ _)
-#align set_like.int_cast_mem_graded SetLike.int_cast_mem_graded
+    exact neg_mem (SetLike.natCast_mem_graded _ _)
+#align set_like.int_cast_mem_graded SetLike.intCast_mem_graded
 
 section DirectSum
 
@@ -106,7 +106,7 @@ instance gsemiring [AddMonoid ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass
     zero_mul := fun _ => Subtype.ext (zero_mul _)
     mul_add := fun _ _ _ => Subtype.ext (mul_add _ _ _)
     add_mul := fun _ _ _ => Subtype.ext (add_mul _ _ _)
-    natCast := fun n => ⟨n, SetLike.nat_cast_mem_graded _ _⟩
+    natCast := fun n => ⟨n, SetLike.natCast_mem_graded _ _⟩
     natCast_zero := Subtype.ext Nat.cast_zero
     natCast_succ := fun n => Subtype.ext (Nat.cast_succ n) }
 #align set_like.gsemiring SetLike.gsemiring
@@ -121,7 +121,7 @@ instance gcommSemiring [AddCommMonoid ι] [CommSemiring R] [SetLike σ R] [AddSu
 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 := fun z => ⟨z, SetLike.intCast_mem_graded _ _⟩
     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/Hom/Instances.lean

@@ -118,10 +118,10 @@ instance AddMonoid.End.instRing [AddCommGroup M] : Ring (AddMonoid.End M) :=
 
 /-- See also `AddMonoid.End.intCast_def`. -/
 @[simp]
-theorem AddMonoid.End.int_cast_apply [AddCommGroup M] (z : ℤ) (m : M) :
+theorem AddMonoid.End.intCast_apply [AddCommGroup M] (z : ℤ) (m : M) :
     (↑z : AddMonoid.End M) m = z • m :=
   rfl
-#align add_monoid.End.int_cast_apply AddMonoid.End.int_cast_apply
+#align add_monoid.End.int_cast_apply AddMonoid.End.intCast_apply
 
 /-!
 ### Morphisms of morphisms

Mathlib/Algebra/Group/InjSurj.lean

@@ -142,11 +142,11 @@ See note [reducible non-instances]. -/
 protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ M₁] [NatCast M₁]
     [AddMonoidWithOne M₂] (f : M₁ → M₂) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (nat_cast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₁ :=
+    (natCast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₁ :=
   { hf.addMonoid f zero add (swap nsmul) with
     natCast := Nat.cast,
-    natCast_zero := hf (by erw [nat_cast, Nat.cast_zero, zero]),
-    natCast_succ := fun n => hf (by erw [nat_cast, Nat.cast_succ, add, one, nat_cast]), one := 1 }
+    natCast_zero := hf (by erw [natCast, Nat.cast_zero, zero]),
+    natCast_succ := fun n => hf (by erw [natCast, Nat.cast_succ, add, one, natCast]), one := 1 }
 #align function.injective.add_monoid_with_one Function.Injective.addMonoidWithOne
 
 /-- A type endowed with `1` and `*` is a left cancel monoid, if it admits an injective map that
@@ -204,8 +204,8 @@ See note [reducible non-instances]. -/
 protected def addCommMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ M₁] [NatCast M₁]
     [AddCommMonoidWithOne M₂] (f : M₁ → M₂) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (nat_cast : ∀ n : ℕ, f n = n) : AddCommMonoidWithOne M₁ where
-  __ := hf.addMonoidWithOne f zero one add nsmul nat_cast
+    (natCast : ∀ n : ℕ, f n = n) : AddCommMonoidWithOne M₁ where
+  __ := hf.addMonoidWithOne f zero one add nsmul natCast
   __ := hf.addCommMonoid _ zero add (swap nsmul)
 #align function.injective.add_comm_monoid_with_one Function.Injective.addCommMonoidWithOne
 
@@ -337,13 +337,13 @@ protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul ℕ
     [SMul ℤ M₁] [NatCast M₁] [IntCast M₁] [AddGroupWithOne M₂] (f : M₁ → M₂) (hf : Injective f)
     (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x)
     (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n)
-    (int_cast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₁ :=
+    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
+    (intCast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₁ :=
   { hf.addGroup f zero add neg sub (swap nsmul) (swap zsmul),
-    hf.addMonoidWithOne f zero one add nsmul nat_cast with
+    hf.addMonoidWithOne f zero one add nsmul natCast with
     intCast := Int.cast,
-    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] ) }
+    intCast_ofNat := fun n => hf (by rw [natCast, ← Int.cast, intCast, Int.cast_natCast]),
+    intCast_negSucc := fun n => hf (by erw [intCast, neg, natCast, Int.cast_negSucc] ) }
 #align function.injective.add_group_with_one Function.Injective.addGroupWithOne
 
 /-- A type endowed with `1`, `*` and `⁻¹` is a commutative group, if it admits an injective map that
@@ -367,9 +367,9 @@ protected def addCommGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul
     [SMul ℤ M₁] [NatCast M₁] [IntCast M₁] [AddCommGroupWithOne M₂] (f : M₁ → M₂) (hf : Injective f)
     (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x)
     (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n)
-    (int_cast : ∀ n : ℤ, f n = n) : AddCommGroupWithOne M₁ :=
-  { hf.addGroupWithOne f zero one add neg sub nsmul zsmul nat_cast int_cast,
+    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
+    (intCast : ∀ n : ℤ, f n = n) : AddCommGroupWithOne M₁ :=
+  { hf.addGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast,
     hf.addCommMonoid _ zero add (swap nsmul) with }
 #align function.injective.add_comm_group_with_one Function.Injective.addCommGroupWithOne
 
@@ -457,11 +457,11 @@ map that preserves `0`, `1` and `*` from an additive monoid with one. See note
 protected def addMonoidWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [SMul ℕ M₂] [NatCast M₂]
     [AddMonoidWithOne M₁] (f : M₁ → M₂) (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (nat_cast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₂ :=
+    (natCast : ∀ n : ℕ, f n = n) : AddMonoidWithOne M₂ :=
   { hf.addMonoid f zero add (swap nsmul) with
     natCast := Nat.cast,
-    natCast_zero := by rw [← Nat.cast, ← nat_cast, Nat.cast_zero, zero]
-    natCast_succ := fun n => by rw [← Nat.cast, ← nat_cast, Nat.cast_succ, add, one, nat_cast]
+    natCast_zero := by rw [← Nat.cast, ← natCast, Nat.cast_zero, zero]
+    natCast_succ := fun n => by rw [← Nat.cast, ← natCast, Nat.cast_succ, add, one, natCast]
     one := 1 }
 #align function.surjective.add_monoid_with_one Function.Surjective.addMonoidWithOne
 
@@ -484,8 +484,8 @@ See note [reducible non-instances]. -/
 protected def addCommMonoidWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [SMul ℕ M₂] [NatCast M₂]
     [AddCommMonoidWithOne M₁] (f : M₁ → M₂) (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (nat_cast : ∀ n : ℕ, f n = n) : AddCommMonoidWithOne M₂ where
-  __ := hf.addMonoidWithOne f zero one add nsmul nat_cast
+    (natCast : ∀ n : ℕ, f n = n) : AddCommMonoidWithOne M₂ where
+  __ := hf.addMonoidWithOne f zero one add nsmul natCast
   __ := hf.addCommMonoid _ zero add (swap nsmul)
 #align function.surjective.add_comm_monoid_with_one Function.Surjective.addCommMonoidWithOne
 
@@ -548,14 +548,14 @@ protected def addGroupWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [Neg M₂
     [SMul ℤ M₂] [NatCast M₂] [IntCast M₂] [AddGroupWithOne M₁] (f : M₁ → M₂) (hf : Surjective f)
     (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x)
     (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n)
-    (int_cast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₂ :=
-  { hf.addMonoidWithOne f zero one add nsmul nat_cast,
+    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
+    (intCast : ∀ n : ℤ, f n = n) : AddGroupWithOne M₂ :=
+  { hf.addMonoidWithOne f zero one add nsmul natCast,
     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_natCast, nat_cast],
+    intCast_ofNat := fun n => by rw [← Int.cast, ← intCast, Int.cast_natCast, natCast],
     intCast_negSucc := fun n => by
-      rw [← Int.cast, ← int_cast, Int.cast_negSucc, neg, nat_cast] }
+      rw [← Int.cast, ← intCast, Int.cast_negSucc, neg, natCast] }
 #align function.surjective.add_group_with_one Function.Surjective.addGroupWithOne
 
 /-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a commutative group, if it admits a surjective
@@ -580,9 +580,9 @@ protected def addCommGroupWithOne {M₂} [Zero M₂] [One M₂] [Add M₂] [Neg
     [SMul ℤ M₂] [NatCast M₂] [IntCast M₂] [AddCommGroupWithOne M₁] (f : M₁ → M₂) (hf : Surjective f)
     (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x)
     (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (nat_cast : ∀ n : ℕ, f n = n)
-    (int_cast : ∀ n : ℤ, f n = n) : AddCommGroupWithOne M₂ :=
-  { hf.addGroupWithOne f zero one add neg sub nsmul zsmul nat_cast int_cast,
+    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
+    (intCast : ∀ n : ℤ, f n = n) : AddCommGroupWithOne M₂ :=
+  { hf.addGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast,
     hf.addCommMonoid _ zero add (swap nsmul) with }
 #align function.surjective.add_comm_group_with_one Function.Surjective.addCommGroupWithOne