From c27bc4e194e730876cdd1f11cd1137bb11e411fb Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 25 Jan 2024 15:54:35 +0000
Subject: [PATCH] refactor(ZMod): remove coe out of ZMod (#9839)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
---
 Mathlib/Data/ZMod/Algebra.lean                |  4 +-
 Mathlib/Data/ZMod/Basic.lean                  | 96 +++++++++----------
 Mathlib/Data/ZMod/Module.lean                 |  4 +-
 Mathlib/Data/ZMod/Quotient.lean               | 10 +-
 Mathlib/Data/ZMod/Units.lean                  |  2 +-
 Mathlib/GroupTheory/Complement.lean           | 14 +--
 .../DirichletCharacter/Basic.lean             |  2 +-
 .../NumberTheory/LegendreSymbol/ZModChar.lean |  2 +-
 Mathlib/NumberTheory/Padics/RingHoms.lean     |  7 +-
 9 files changed, 71 insertions(+), 70 deletions(-)

diff --git a/Mathlib/Data/ZMod/Algebra.lean b/Mathlib/Data/ZMod/Algebra.lean
index ff3c05c6c2d91..3f1f4e734f1e7 100644
--- a/Mathlib/Data/ZMod/Algebra.lean
+++ b/Mathlib/Data/ZMod/Algebra.lean
@@ -29,9 +29,9 @@ See note [reducible non-instances]. -/
 @[reducible]
 def algebra' (h : m ∣ n) : Algebra (ZMod n) R :=
   { ZMod.castHom h R with
-    smul := fun a r => a * r
+    smul := fun a r => cast a * r
     commutes' := fun a r =>
-      show (a * r : R) = r * a by
+      show (cast a * r : R) = r * cast a by
         rcases ZMod.int_cast_surjective a with ⟨k, rfl⟩
         show ZMod.castHom h R k * r = r * ZMod.castHom h R k
         rw [map_intCast, Int.cast_comm]
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index 6e32452d2f1f6..0c5e2ed707aa1 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -148,24 +148,21 @@ variable [AddGroupWithOne R]
 /-- Cast an integer modulo `n` to another semiring.
 This function is a morphism if the characteristic of `R` divides `n`.
 See `ZMod.castHom` for a bundled version. -/
-@[coe] def cast : ∀ {n : ℕ}, ZMod n → R
+def cast : ∀ {n : ℕ}, ZMod n → R
   | 0 => Int.cast
   | _ + 1 => fun i => i.val
 #align zmod.cast ZMod.cast
 
--- see Note [coercion into rings]
-instance (priority := 900) (n : ℕ) : CoeTC (ZMod n) R :=
-  ⟨cast⟩
 
 @[simp]
-theorem cast_zero : ((0 : ZMod n) : R) = 0 := by
+theorem cast_zero : (cast (0 : ZMod n) : R) = 0 := by
   delta ZMod.cast
   cases n
   · exact Int.cast_zero
   · simp
 #align zmod.cast_zero ZMod.cast_zero
 
-theorem cast_eq_val [NeZero n] (a : ZMod n) : (a : R) = a.val := by
+theorem cast_eq_val [NeZero n] (a : ZMod n) : (cast a : R) = a.val := by
   cases n
   · cases NeZero.ne 0 rfl
   rfl
@@ -174,14 +171,14 @@ theorem cast_eq_val [NeZero n] (a : ZMod n) : (a : R) = a.val := by
 variable {S : Type*} [AddGroupWithOne S]
 
 @[simp]
-theorem _root_.Prod.fst_zmod_cast (a : ZMod n) : (a : R × S).fst = a := by
+theorem _root_.Prod.fst_zmod_cast (a : ZMod n) : (cast a : R × S).fst = cast a := by
   cases n
   · rfl
   · simp [ZMod.cast]
 #align prod.fst_zmod_cast Prod.fst_zmod_cast
 
 @[simp]
-theorem _root_.Prod.snd_zmod_cast (a : ZMod n) : (a : R × S).snd = a := by
+theorem _root_.Prod.snd_zmod_cast (a : ZMod n) : (cast a : R × S).snd = cast a := by
   cases n
   · rfl
   · simp [ZMod.cast]
@@ -208,14 +205,14 @@ theorem nat_cast_zmod_surjective [NeZero n] : Function.Surjective ((↑) : ℕ 
 /-- So-named because the outer coercion is `Int.cast` into `ZMod`. For `Int.cast` into an arbitrary
 ring, see `ZMod.int_cast_cast`. -/
 @[norm_cast]
-theorem int_cast_zmod_cast (a : ZMod n) : ((a : ℤ) : ZMod n) = a := by
+theorem int_cast_zmod_cast (a : ZMod n) : ((cast a : ℤ) : ZMod n) = a := by
   cases n
   · simp [ZMod.cast, ZMod]
   · dsimp [ZMod.cast, ZMod]
     erw [Int.cast_ofNat, Fin.cast_val_eq_self]
 #align zmod.int_cast_zmod_cast ZMod.int_cast_zmod_cast
 
-theorem int_cast_rightInverse : Function.RightInverse ((↑) : ZMod n → ℤ) ((↑) : ℤ → ZMod n) :=
+theorem int_cast_rightInverse : Function.RightInverse (cast : ZMod n → ℤ) ((↑) : ℤ → ZMod n) :=
   int_cast_zmod_cast
 #align zmod.int_cast_right_inverse ZMod.int_cast_rightInverse
 
@@ -223,7 +220,6 @@ theorem int_cast_surjective : Function.Surjective ((↑) : ℤ → ZMod n) :=
   int_cast_rightInverse.surjective
 #align zmod.int_cast_surjective ZMod.int_cast_surjective
 
-@[norm_cast]
 theorem cast_id : ∀ (n) (i : ZMod n), (ZMod.cast i : ZMod n) = i
   | 0, _ => Int.cast_id
   | _ + 1, i => nat_cast_zmod_val i
@@ -238,7 +234,7 @@ variable (R) [Ring R]
 
 /-- The coercions are respectively `Nat.cast` and `ZMod.cast`. -/
 @[simp]
-theorem nat_cast_comp_val [NeZero n] : ((↑) : ℕ → R) ∘ (val : ZMod n → ℕ) = (↑) := by
+theorem nat_cast_comp_val [NeZero n] : ((↑) : ℕ → R) ∘ (val : ZMod n → ℕ) = cast := by
   cases n
   · cases NeZero.ne 0 rfl
   rfl
@@ -246,7 +242,7 @@ theorem nat_cast_comp_val [NeZero n] : ((↑) : ℕ → R) ∘ (val : ZMod n →
 
 /-- The coercions are respectively `Int.cast`, `ZMod.cast`, and `ZMod.cast`. -/
 @[simp]
-theorem int_cast_comp_cast : ((↑) : ℤ → R) ∘ ((↑) : ZMod n → ℤ) = (↑) := by
+theorem int_cast_comp_cast : ((↑) : ℤ → R) ∘ (cast : ZMod n → ℤ) = cast := by
   cases n
   · exact congr_arg (Int.cast ∘ ·) ZMod.cast_id'
   · ext
@@ -256,17 +252,18 @@ theorem int_cast_comp_cast : ((↑) : ℤ → R) ∘ ((↑) : ZMod n → ℤ) =
 variable {R}
 
 @[simp]
-theorem nat_cast_val [NeZero n] (i : ZMod n) : (i.val : R) = i :=
+theorem nat_cast_val [NeZero n] (i : ZMod n) : (i.val : R) = cast i :=
   congr_fun (nat_cast_comp_val R) i
 #align zmod.nat_cast_val ZMod.nat_cast_val
 
 @[simp]
-theorem int_cast_cast (i : ZMod n) : ((i : ℤ) : R) = i :=
+theorem int_cast_cast (i : ZMod n) : ((cast i : ℤ) : R) = cast i :=
   congr_fun (int_cast_comp_cast R) i
 #align zmod.int_cast_cast ZMod.int_cast_cast
 
-theorem coe_add_eq_ite {n : ℕ} (a b : ZMod n) :
-    (↑(a + b) : ℤ) = if (n : ℤ) ≤ a + b then (a : ℤ) + b - n else a + b := by
+theorem cast_add_eq_ite {n : ℕ} (a b : ZMod n) :
+    (cast (a + b) : ℤ) =
+      if (n : ℤ) ≤ cast a + cast b then (cast a + cast b - n : ℤ) else cast a + cast b := by
   cases' n with n
   · simp; rfl
   change Fin (n + 1) at a b
@@ -277,7 +274,7 @@ theorem coe_add_eq_ite {n : ℕ} (a b : ZMod n) :
   · rw [Nat.cast_sub h]
     congr
   · rfl
-#align zmod.coe_add_eq_ite ZMod.coe_add_eq_ite
+#align zmod.coe_add_eq_ite ZMod.cast_add_eq_ite
 
 section CharDvd
 
@@ -287,7 +284,7 @@ section CharDvd
 variable {m : ℕ} [CharP R m]
 
 @[simp]
-theorem cast_one (h : m ∣ n) : ((1 : ZMod n) : R) = 1 := by
+theorem cast_one (h : m ∣ n) : (cast (1 : ZMod n) : R) = 1 := by
   cases' n with n
   · exact Int.cast_one
   show ((1 % (n + 1) : ℕ) : R) = 1
@@ -300,7 +297,7 @@ theorem cast_one (h : m ∣ n) : ((1 : ZMod n) : R) = 1 := by
   exact Nat.lt_of_sub_eq_succ rfl
 #align zmod.cast_one ZMod.cast_one
 
-theorem cast_add (h : m ∣ n) (a b : ZMod n) : ((a + b : ZMod n) : R) = a + b := by
+theorem cast_add (h : m ∣ n) (a b : ZMod n) : (cast (a + b : ZMod n) : R) = cast a + cast b := by
   cases n
   · apply Int.cast_add
   symm
@@ -310,7 +307,7 @@ theorem cast_add (h : m ∣ n) (a b : ZMod n) : ((a + b : ZMod n) : R) = a + b :
   exact h.trans (Nat.dvd_sub_mod _)
 #align zmod.cast_add ZMod.cast_add
 
-theorem cast_mul (h : m ∣ n) (a b : ZMod n) : ((a * b : ZMod n) : R) = a * b := by
+theorem cast_mul (h : m ∣ n) (a b : ZMod n) : (cast (a * b : ZMod n) : R) = cast a * cast b := by
   cases n
   · apply Int.cast_mul
   symm
@@ -325,7 +322,7 @@ theorem cast_mul (h : m ∣ n) (a b : ZMod n) : ((a * b : ZMod n) : R) = a * b :
 See also `ZMod.lift` for a generalized version working in `AddGroup`s.
 -/
 def castHom (h : m ∣ n) (R : Type*) [Ring R] [CharP R m] : ZMod n →+* R where
-  toFun := (↑)
+  toFun := cast
   map_zero' := cast_zero
   map_one' := cast_one h
   map_add' := cast_add h
@@ -333,32 +330,32 @@ def castHom (h : m ∣ n) (R : Type*) [Ring R] [CharP R m] : ZMod n →+* R wher
 #align zmod.cast_hom ZMod.castHom
 
 @[simp]
-theorem castHom_apply {h : m ∣ n} (i : ZMod n) : castHom h R i = i :=
+theorem castHom_apply {h : m ∣ n} (i : ZMod n) : castHom h R i = cast i :=
   rfl
 #align zmod.cast_hom_apply ZMod.castHom_apply
 
-@[simp, norm_cast]
-theorem cast_sub (h : m ∣ n) (a b : ZMod n) : ((a - b : ZMod n) : R) = (a : R) - b :=
+@[simp]
+theorem cast_sub (h : m ∣ n) (a b : ZMod n) : (cast (a - b : ZMod n) : R) = cast a - cast b :=
   (castHom h R).map_sub a b
 #align zmod.cast_sub ZMod.cast_sub
 
-@[simp, norm_cast]
-theorem cast_neg (h : m ∣ n) (a : ZMod n) : ((-a : ZMod n) : R) = -(a : R) :=
+@[simp]
+theorem cast_neg (h : m ∣ n) (a : ZMod n) : (cast (-a : ZMod n) : R) = -(cast a) :=
   (castHom h R).map_neg a
 #align zmod.cast_neg ZMod.cast_neg
 
-@[simp, norm_cast]
-theorem cast_pow (h : m ∣ n) (a : ZMod n) (k : ℕ) : ((a ^ k : ZMod n) : R) = (a : R) ^ k :=
+@[simp]
+theorem cast_pow (h : m ∣ n) (a : ZMod n) (k : ℕ) : (cast (a ^ k : ZMod n) : R) = (cast a) ^ k :=
   (castHom h R).map_pow a k
 #align zmod.cast_pow ZMod.cast_pow
 
 @[simp, norm_cast]
-theorem cast_nat_cast (h : m ∣ n) (k : ℕ) : ((k : ZMod n) : R) = k :=
+theorem cast_nat_cast (h : m ∣ n) (k : ℕ) : (cast (k : ZMod n) : R) = k :=
   map_natCast (castHom h R) k
 #align zmod.cast_nat_cast ZMod.cast_nat_cast
 
 @[simp, norm_cast]
-theorem cast_int_cast (h : m ∣ n) (k : ℤ) : ((k : ZMod n) : R) = k :=
+theorem cast_int_cast (h : m ∣ n) (k : ℤ) : (cast (k : ZMod n) : R) = k :=
   map_intCast (castHom h R) k
 #align zmod.cast_int_cast ZMod.cast_int_cast
 
@@ -372,37 +369,37 @@ section CharEq
 variable [CharP R n]
 
 @[simp]
-theorem cast_one' : ((1 : ZMod n) : R) = 1 :=
+theorem cast_one' : (cast (1 : ZMod n) : R) = 1 :=
   cast_one dvd_rfl
 #align zmod.cast_one' ZMod.cast_one'
 
 @[simp]
-theorem cast_add' (a b : ZMod n) : ((a + b : ZMod n) : R) = a + b :=
+theorem cast_add' (a b : ZMod n) : (cast (a + b : ZMod n) : R) = cast a + cast b :=
   cast_add dvd_rfl a b
 #align zmod.cast_add' ZMod.cast_add'
 
 @[simp]
-theorem cast_mul' (a b : ZMod n) : ((a * b : ZMod n) : R) = a * b :=
+theorem cast_mul' (a b : ZMod n) : (cast (a * b : ZMod n) : R) = cast a * cast b :=
   cast_mul dvd_rfl a b
 #align zmod.cast_mul' ZMod.cast_mul'
 
 @[simp]
-theorem cast_sub' (a b : ZMod n) : ((a - b : ZMod n) : R) = a - b :=
+theorem cast_sub' (a b : ZMod n) : (cast (a - b : ZMod n) : R) = cast a - cast b :=
   cast_sub dvd_rfl a b
 #align zmod.cast_sub' ZMod.cast_sub'
 
 @[simp]
-theorem cast_pow' (a : ZMod n) (k : ℕ) : ((a ^ k : ZMod n) : R) = (a : R) ^ k :=
+theorem cast_pow' (a : ZMod n) (k : ℕ) : (cast (a ^ k : ZMod n) : R) = (cast a : R) ^ k :=
   cast_pow dvd_rfl a k
 #align zmod.cast_pow' ZMod.cast_pow'
 
 @[simp, norm_cast]
-theorem cast_nat_cast' (k : ℕ) : ((k : ZMod n) : R) = k :=
+theorem cast_nat_cast' (k : ℕ) : (cast (k : ZMod n) : R) = k :=
   cast_nat_cast dvd_rfl k
 #align zmod.cast_nat_cast' ZMod.cast_nat_cast'
 
 @[simp, norm_cast]
-theorem cast_int_cast' (k : ℤ) : ((k : ZMod n) : R) = k :=
+theorem cast_int_cast' (k : ℤ) : (cast (k : ZMod n) : R) = k :=
   cast_int_cast dvd_rfl k
 #align zmod.cast_int_cast' ZMod.cast_int_cast'
 
@@ -492,7 +489,7 @@ theorem val_int_cast {n : ℕ} (a : ℤ) [NeZero n] : ↑(a : ZMod n).val = a %
   rw [← ZMod.int_cast_eq_int_cast_iff', Int.cast_ofNat, ZMod.nat_cast_val, ZMod.cast_id]
 #align zmod.val_int_cast ZMod.val_int_cast
 
-theorem coe_int_cast {n : ℕ} (a : ℤ) : ↑(a : ZMod n) = a % n := by
+theorem coe_int_cast {n : ℕ} (a : ℤ) : cast (a : ZMod n) = a % n := by
   cases n
   · rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]; rfl
   · rw [← val_int_cast, val]; rfl
@@ -508,14 +505,14 @@ theorem val_neg_one (n : ℕ) : (-1 : ZMod n.succ).val = n := by
 #align zmod.val_neg_one ZMod.val_neg_one
 
 /-- `-1 : ZMod n` lifts to `n - 1 : R`. This avoids the characteristic assumption in `cast_neg`. -/
-theorem cast_neg_one {R : Type*} [Ring R] (n : ℕ) : ↑(-1 : ZMod n) = (n - 1 : R) := by
+theorem cast_neg_one {R : Type*} [Ring R] (n : ℕ) : cast (-1 : ZMod n) = (n - 1 : R) := by
   cases' n with n
   · dsimp [ZMod, ZMod.cast]; simp
   · rw [← nat_cast_val, val_neg_one, Nat.cast_succ, add_sub_cancel]
 #align zmod.cast_neg_one ZMod.cast_neg_one
 
 theorem cast_sub_one {R : Type*} [Ring R] {n : ℕ} (k : ZMod n) :
-    ((k - 1 : ZMod n) : R) = (if k = 0 then (n : R) else k) - 1 := by
+    (cast (k - 1 : ZMod n) : R) = (if k = 0 then (n : R) else cast k) - 1 := by
   split_ifs with hk
   · rw [hk, zero_sub, ZMod.cast_neg_one]
   · cases n
@@ -581,7 +578,7 @@ theorem cast_injective_of_le {m n : ℕ} [nzm : NeZero m] (h : m ≤ n) :
     exact f
 
 theorem cast_zmod_eq_zero_iff_of_le {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ZMod m) :
-    (a : ZMod n) = 0 ↔ a = 0 := by
+    (cast a : ZMod n) = 0 ↔ a = 0 := by
   rw [← ZMod.cast_zero (n := m)]
   exact Injective.eq_iff' (cast_injective_of_le h) rfl
 
@@ -798,7 +795,8 @@ def chineseRemainder {m n : ℕ} (h : m.Coprime n) : ZMod (m * n) ≃+* ZMod m 
   let to_fun : ZMod (m * n) → ZMod m × ZMod n :=
     ZMod.castHom (show m.lcm n ∣ m * n by simp [Nat.lcm_dvd_iff]) (ZMod m × ZMod n)
   let inv_fun : ZMod m × ZMod n → ZMod (m * n) := fun x =>
-    if m * n = 0 then if m = 1 then RingHom.snd _ (ZMod n) x else RingHom.fst (ZMod m) _ x
+    if m * n = 0 then
+      if m = 1 then cast (RingHom.snd _ (ZMod n) x) else cast (RingHom.fst (ZMod m) _ x)
     else Nat.chineseRemainder h x.1.val x.2.val
   have inv : Function.LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun :=
     if hmn0 : m * n = 0 then by
@@ -824,8 +822,8 @@ def chineseRemainder {m n : ℕ} (h : m.Coprime n) : ZMod (m * n) ≃+* ZMod m 
         rw [if_neg hmn0, ZMod.eq_iff_modEq_nat, ← Nat.modEq_and_modEq_iff_modEq_mul h,
           Prod.fst_zmod_cast, Prod.snd_zmod_cast]
         refine'
-          ⟨(Nat.chineseRemainder h (x : ZMod m).val (x : ZMod n).val).2.left.trans _,
-            (Nat.chineseRemainder h (x : ZMod m).val (x : ZMod n).val).2.right.trans _⟩
+          ⟨(Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.left.trans _,
+            (Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.right.trans _⟩
         · rw [← ZMod.eq_iff_modEq_nat, ZMod.nat_cast_zmod_val, ZMod.nat_cast_val]
         · rw [← ZMod.eq_iff_modEq_nat, ZMod.nat_cast_zmod_val, ZMod.nat_cast_val]
       exact ⟨left_inv, left_inv.rightInverse_of_card_le (by simp)⟩
@@ -953,7 +951,7 @@ theorem val_cast_eq_val_of_lt {m n : ℕ} [nzm : NeZero m] {a : ZMod m}
     | succ n => exact Fin.val_cast_of_lt h
 
 theorem cast_cast_zmod_of_le {m n : ℕ} [hm : NeZero m] (h : m ≤ n) (a : ZMod m) :
-    ((a : ZMod n) : ZMod m) = a := by
+    (cast (cast a : ZMod n) : ZMod m) = a := by
   have : NeZero n := ⟨((Nat.zero_lt_of_ne_zero hm.out).trans_le h).ne'⟩
   rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), nat_cast_zmod_val]
 
@@ -1222,7 +1220,7 @@ instance subsingleton_ringEquiv [Semiring R] : Subsingleton (ZMod n ≃+* R) :=
 #align zmod.subsingleton_ring_equiv ZMod.subsingleton_ringEquiv
 
 @[simp]
-theorem ringHom_map_cast [Ring R] (f : R →+* ZMod n) (k : ZMod n) : f k = k := by
+theorem ringHom_map_cast [Ring R] (f : R →+* ZMod n) (k : ZMod n) : f (cast k) = k := by
   cases n
   · dsimp [ZMod, ZMod.cast] at f k ⊢; simp
   · dsimp [ZMod, ZMod.cast] at f k ⊢
@@ -1230,7 +1228,7 @@ theorem ringHom_map_cast [Ring R] (f : R →+* ZMod n) (k : ZMod n) : f k = k :=
 #align zmod.ring_hom_map_cast ZMod.ringHom_map_cast
 
 theorem ringHom_rightInverse [Ring R] (f : R →+* ZMod n) :
-    Function.RightInverse ((↑) : ZMod n → R) f :=
+    Function.RightInverse (cast : ZMod n → R) f :=
   ringHom_map_cast f
 #align zmod.ring_hom_right_inverse ZMod.ringHom_rightInverse
 
@@ -1269,7 +1267,7 @@ def lift : { f : ℤ →+ A // f n = 0 } ≃ (ZMod n →+ A) :=
           simp only [f.map_zsmul, zsmul_zero, f.mem_ker, hf]
         · intro h
           refine' h (AddSubgroup.mem_zmultiples _)).trans <|
-    (Int.castAddHom (ZMod n)).liftOfRightInverse (↑) int_cast_zmod_cast
+    (Int.castAddHom (ZMod n)).liftOfRightInverse cast int_cast_zmod_cast
 #align zmod.lift ZMod.lift
 
 variable (f : { f : ℤ →+ A // f n = 0 })
diff --git a/Mathlib/Data/ZMod/Module.lean b/Mathlib/Data/ZMod/Module.lean
index 7fca517aebab1..7936bc16ef132 100644
--- a/Mathlib/Data/ZMod/Module.lean
+++ b/Mathlib/Data/ZMod/Module.lean
@@ -48,11 +48,11 @@ namespace ZMod
 
 theorem map_smul (f : F) (c : ZMod n) (x : M) : f (c • x) = c • f x := by
   rw [← ZMod.int_cast_zmod_cast c]
-  exact map_int_cast_smul f _ _ c x
+  exact map_int_cast_smul f _ _ (cast c) x
 
 theorem smul_mem (hx : x ∈ K) (c : ZMod n) : c • x ∈ K := by
   rw [← ZMod.int_cast_zmod_cast c, ← zsmul_eq_smul_cast]
-  exact zsmul_mem hx c
+  exact zsmul_mem hx (cast c)
 
 end ZMod
 
diff --git a/Mathlib/Data/ZMod/Quotient.lean b/Mathlib/Data/ZMod/Quotient.lean
index 8a53edb36018f..482e34b05aed8 100644
--- a/Mathlib/Data/ZMod/Quotient.lean
+++ b/Mathlib/Data/ZMod/Quotient.lean
@@ -43,7 +43,7 @@ namespace Int
 /-- `ℤ` modulo multiples of `n : ℕ` is `ZMod n`. -/
 def quotientZMultiplesNatEquivZMod : ℤ ⧸ AddSubgroup.zmultiples (n : ℤ) ≃+ ZMod n :=
   (quotientAddEquivOfEq (ZMod.ker_int_castAddHom _)).symm.trans <|
-    quotientKerEquivOfRightInverse (Int.castAddHom (ZMod n)) (↑) int_cast_zmod_cast
+    quotientKerEquivOfRightInverse (Int.castAddHom (ZMod n)) cast int_cast_zmod_cast
 #align int.quotient_zmultiples_nat_equiv_zmod Int.quotientZMultiplesNatEquivZMod
 
 /-- `ℤ` modulo multiples of `a : ℤ` is `ZMod a.nat_abs`. -/
@@ -55,7 +55,7 @@ def quotientZMultiplesEquivZMod (a : ℤ) : ℤ ⧸ AddSubgroup.zmultiples a ≃
 def quotientSpanNatEquivZMod : ℤ ⧸ Ideal.span {(n : ℤ)} ≃+* ZMod n :=
   (Ideal.quotEquivOfEq (ZMod.ker_int_castRingHom _)).symm.trans <|
     RingHom.quotientKerEquivOfRightInverse <|
-      show Function.RightInverse (↑) (Int.castRingHom (ZMod n)) from int_cast_zmod_cast
+      show Function.RightInverse ZMod.cast (Int.castRingHom (ZMod n)) from int_cast_zmod_cast
 #align int.quotient_span_nat_equiv_zmod Int.quotientSpanNatEquivZMod
 
 /-- `ℤ` modulo the ideal generated by `a : ℤ` is `ZMod a.nat_abs`. -/
@@ -108,7 +108,7 @@ noncomputable def zmultiplesQuotientStabilizerEquiv :
 
 theorem zmultiplesQuotientStabilizerEquiv_symm_apply (n : ZMod (minimalPeriod (a +ᵥ ·) b)) :
     (zmultiplesQuotientStabilizerEquiv a b).symm n =
-      (n : ℤ) • (⟨a, mem_zmultiples a⟩ : zmultiples a) :=
+      (cast n : ℤ) • (⟨a, mem_zmultiples a⟩ : zmultiples a) :=
   rfl
 #align add_action.zmultiples_quotient_stabilizer_equiv_symm_apply AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply
 
@@ -128,7 +128,7 @@ noncomputable def zpowersQuotientStabilizerEquiv :
 #align mul_action.zpowers_quotient_stabilizer_equiv MulAction.zpowersQuotientStabilizerEquiv
 
 theorem zpowersQuotientStabilizerEquiv_symm_apply (n : ZMod (minimalPeriod (a • ·) b)) :
-    (zpowersQuotientStabilizerEquiv a b).symm n = (⟨a, mem_zpowers a⟩ : zpowers a) ^ (n : ℤ) :=
+    (zpowersQuotientStabilizerEquiv a b).symm n = (⟨a, mem_zpowers a⟩ : zpowers a) ^ (cast n : ℤ) :=
   rfl
 #align mul_action.zpowers_quotient_stabilizer_equiv_symm_apply MulAction.zpowersQuotientStabilizerEquiv_symm_apply
 
@@ -150,7 +150,7 @@ attribute [to_additive existing AddAction.orbitZMultiplesEquiv] orbitZPowersEqui
 @[to_additive orbit_zmultiples_equiv_symm_apply]
 theorem orbitZPowersEquiv_symm_apply (k : ZMod (minimalPeriod (a • ·) b)) :
     (orbitZPowersEquiv a b).symm k =
-      (⟨a, mem_zpowers a⟩ : zpowers a) ^ (k : ℤ) • ⟨b, mem_orbit_self b⟩ :=
+      (⟨a, mem_zpowers a⟩ : zpowers a) ^ (cast k : ℤ) • ⟨b, mem_orbit_self b⟩ :=
   rfl
 #align mul_action.orbit_zpowers_equiv_symm_apply MulAction.orbitZPowersEquiv_symm_apply
 #align add_action.orbit_zmultiples_equiv_symm_apply AddAction.orbit_zmultiples_equiv_symm_apply
diff --git a/Mathlib/Data/ZMod/Units.lean b/Mathlib/Data/ZMod/Units.lean
index b595a21592145..61b905956baef 100644
--- a/Mathlib/Data/ZMod/Units.lean
+++ b/Mathlib/Data/ZMod/Units.lean
@@ -32,7 +32,7 @@ lemma unitsMap_comp {d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
 lemma unitsMap_self (n : ℕ) : unitsMap (dvd_refl n) = MonoidHom.id _ := by
   simp [unitsMap, castHom_self]
 
-lemma IsUnit_cast_of_dvd (hm : n ∣ m) (a : Units (ZMod m)) : IsUnit ((a : ZMod m) : ZMod n) :=
+lemma IsUnit_cast_of_dvd (hm : n ∣ m) (a : Units (ZMod m)) : IsUnit (cast (a : ZMod m) : ZMod n) :=
   Units.isUnit (unitsMap hm a)
 
 theorem unitsMap_surjective [hm : NeZero m] (h : n ∣ m) :
diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean
index b6aef88c20e3f..9d6350bf654db 100644
--- a/Mathlib/GroupTheory/Complement.lean
+++ b/Mathlib/GroupTheory/Complement.lean
@@ -767,7 +767,7 @@ noncomputable def quotientEquivSigmaZMod :
 
 theorem quotientEquivSigmaZMod_symm_apply (q : orbitRel.Quotient (zpowers g) (G ⧸ H))
     (k : ZMod (minimalPeriod (g • ·) q.out')) :
-    (quotientEquivSigmaZMod H g).symm ⟨q, k⟩ = g ^ (k : ℤ) • q.out' :=
+    (quotientEquivSigmaZMod H g).symm ⟨q, k⟩ = g ^ (cast k : ℤ) • q.out' :=
   rfl
 #align subgroup.quotient_equiv_sigma_zmod_symm_apply Subgroup.quotientEquivSigmaZMod_symm_apply
 
@@ -781,12 +781,13 @@ theorem quotientEquivSigmaZMod_apply (q : orbitRel.Quotient (zpowers g) (G ⧸ H
   in `G ⧸ H`, an element `g ^ k • q₀` is mapped to `g ^ k • g₀` for a fixed choice of
   representative `g₀` of `q₀`. -/
 noncomputable def transferFunction : G ⧸ H → G := fun q =>
-  g ^ ((quotientEquivSigmaZMod H g q).2 : ℤ) * (quotientEquivSigmaZMod H g q).1.out'.out'
+  g ^ (cast (quotientEquivSigmaZMod H g q).2 : ℤ) * (quotientEquivSigmaZMod H g q).1.out'.out'
 #align subgroup.transfer_function Subgroup.transferFunction
 
 theorem transferFunction_apply (q : G ⧸ H) :
     transferFunction H g q =
-      g ^ ((quotientEquivSigmaZMod H g q).2 : ℤ) * (quotientEquivSigmaZMod H g q).1.out'.out' :=
+      g ^ (cast (quotientEquivSigmaZMod H g q).2 : ℤ) *
+        (quotientEquivSigmaZMod H g q).1.out'.out' :=
   rfl
 #align subgroup.transfer_function_apply Subgroup.transferFunction_apply
 
@@ -818,16 +819,17 @@ theorem transferTransversal_apply (q : G ⧸ H) :
 
 theorem transferTransversal_apply' (q : orbitRel.Quotient (zpowers g) (G ⧸ H))
     (k : ZMod (minimalPeriod (g • ·) q.out')) :
-    ↑(toEquiv (transferTransversal H g).2 (g ^ (k : ℤ) • q.out')) = g ^ (k : ℤ) * q.out'.out' := by
+    ↑(toEquiv (transferTransversal H g).2 (g ^ (cast k : ℤ) • q.out')) =
+      g ^ (cast k : ℤ) * q.out'.out' := by
   rw [transferTransversal_apply, transferFunction_apply, ← quotientEquivSigmaZMod_symm_apply,
     apply_symm_apply]
 #align subgroup.transfer_transversal_apply' Subgroup.transferTransversal_apply'
 
 theorem transferTransversal_apply'' (q : orbitRel.Quotient (zpowers g) (G ⧸ H))
     (k : ZMod (minimalPeriod (g • ·) q.out')) :
-    ↑(toEquiv (g • transferTransversal H g).2 (g ^ (k : ℤ) • q.out')) =
+    ↑(toEquiv (g • transferTransversal H g).2 (g ^ (cast k : ℤ) • q.out')) =
       if k = 0 then g ^ minimalPeriod (g • ·) q.out' * q.out'.out'
-      else g ^ (k : ℤ) * q.out'.out' := by
+      else g ^ (cast k : ℤ) * q.out'.out' := by
   rw [smul_apply_eq_smul_apply_inv_smul, transferTransversal_apply, transferFunction_apply, ←
     mul_smul, ← zpow_neg_one, ← zpow_add, quotientEquivSigmaZMod_apply, smul_eq_mul, ← mul_assoc,
     ← zpow_one_add, Int.cast_add, Int.cast_neg, Int.cast_one, int_cast_cast, cast_id', id.def, ←
diff --git a/Mathlib/NumberTheory/DirichletCharacter/Basic.lean b/Mathlib/NumberTheory/DirichletCharacter/Basic.lean
index c2cadaef1b099..17f5ab9c6f57b 100644
--- a/Mathlib/NumberTheory/DirichletCharacter/Basic.lean
+++ b/Mathlib/NumberTheory/DirichletCharacter/Basic.lean
@@ -86,7 +86,7 @@ lemma changeLevel_trans {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
   simp [changeLevel_def, MonoidHom.comp_assoc, ZMod.unitsMap_comp]
 
 lemma changeLevel_eq_cast_of_dvd {m : ℕ} (hm : n ∣ m) (a : Units (ZMod m)) :
-    (changeLevel hm χ) a = χ a := by
+    (changeLevel hm χ) a = χ (ZMod.cast (a : ZMod m)) := by
   simpa [changeLevel_def, Function.comp_apply, MonoidHom.coe_comp] using
       toUnitHom_eq_char' _ <| ZMod.IsUnit_cast_of_dvd hm a
 
diff --git a/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean b/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
index 920e8af712f16..f7080591e58f4 100644
--- a/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
+++ b/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
@@ -205,7 +205,7 @@ theorem χ₈'_nat_eq_if_mod_eight (n : ℕ) :
 #align zmod.χ₈'_nat_eq_if_mod_eight ZMod.χ₈'_nat_eq_if_mod_eight
 
 /-- The relation between `χ₄`, `χ₈` and `χ₈'` -/
-theorem χ₈'_eq_χ₄_mul_χ₈ (a : ZMod 8) : χ₈' a = χ₄ a * χ₈ a := by
+theorem χ₈'_eq_χ₄_mul_χ₈ (a : ZMod 8) : χ₈' a = χ₄ (cast a) * χ₈ a := by
     --porting note: was `decide!`
   fin_cases a
   all_goals decide
diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean
index 2caefc0436765..8878b542a96ef 100644
--- a/Mathlib/NumberTheory/Padics/RingHoms.lean
+++ b/Mathlib/NumberTheory/Padics/RingHoms.lean
@@ -269,7 +269,7 @@ to coerce to rings of arbitrary characteristic, instead of only rings of charact
 This coercion is only a ring homomorphism if it coerces into a ring whose characteristic divides
 `p`. While this is not the case here we can still make use of the coercion.
 -/
-theorem toZMod_spec : x - (toZMod x : ℤ_[p]) ∈ maximalIdeal ℤ_[p] := by
+theorem toZMod_spec : x - (ZMod.cast (toZMod x) : ℤ_[p]) ∈ maximalIdeal ℤ_[p] := by
   convert sub_zmodRepr_mem x using 2
   dsimp [toZMod, toZModHom]
   rcases exists_eq_add_of_lt hp_prime.1.pos with ⟨p', rfl⟩
@@ -441,7 +441,8 @@ theorem zmod_cast_comp_toZModPow (m n : ℕ) (h : m ≤ n) :
 #align padic_int.zmod_cast_comp_to_zmod_pow PadicInt.zmod_cast_comp_toZModPow
 
 @[simp]
-theorem cast_toZModPow (m n : ℕ) (h : m ≤ n) (x : ℤ_[p]) : ↑(toZModPow n x) = toZModPow m x := by
+theorem cast_toZModPow (m n : ℕ) (h : m ≤ n) (x : ℤ_[p]) :
+    ZMod.cast (toZModPow n x) = toZModPow m x := by
   rw [← zmod_cast_comp_toZModPow _ _ h]
   rfl
 #align padic_int.cast_to_zmod_pow PadicInt.cast_toZModPow
@@ -533,7 +534,7 @@ theorem nthHomSeq_one : nthHomSeq f_compat 1 ≈ 1 := by
   use 1
   intro j hj
   haveI : Fact (1 < p ^ j) := ⟨Nat.one_lt_pow _ _ (by linarith) hp_prime.1.one_lt⟩
-  suffices ((1 : ZMod (p ^ j)) : ℚ) = 1 by simp [nthHomSeq, nthHom, this, hε]
+  suffices (ZMod.cast (1 : ZMod (p ^ j)) : ℚ) = 1 by simp [nthHomSeq, nthHom, this, hε]
   rw [ZMod.cast_eq_val, ZMod.val_one, Nat.cast_one]
 #align padic_int.nth_hom_seq_one PadicInt.nthHomSeq_one