chore: replace exact_mod_cast tactic with mod_cast elaborator whe…

…re possible (#8404)

We still have the `exact_mod_cast` tactic, used in a few places, which somehow (?) works a little bit harder to prevent the expected type influencing the elaboration of the term. I would like to get to the bottom of this, and it will be easier once the only usages of `exact_mod_cast` are the ones that don't work using the term elaborator by itself.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Archive/Imo/Imo1981Q3.lean

@@ -97,25 +97,25 @@ namespace NatPredicate
 
 variable {N}
 
-nonrec theorem m_le_n {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ n := by exact_mod_cast h1.m_le_n
+nonrec theorem m_le_n {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ n := mod_cast h1.m_le_n
 #align imo1981_q3.nat_predicate.m_le_n Imo1981Q3.NatPredicate.m_le_n
 
-nonrec theorem eq_imp_1 {n : ℕ} (h1 : NatPredicate N n n) : n = 1 := by exact_mod_cast h1.eq_imp_1
+nonrec theorem eq_imp_1 {n : ℕ} (h1 : NatPredicate N n n) : n = 1 := mod_cast h1.eq_imp_1
 #align imo1981_q3.nat_predicate.eq_imp_1 Imo1981Q3.NatPredicate.eq_imp_1
 
 nonrec theorem reduction {m n : ℕ} (h1 : NatPredicate N m n) (h2 : 1 < n) :
     NatPredicate N (n - m) m := by
   have : m ≤ n := h1.m_le_n
-  exact_mod_cast h1.reduction (by exact_mod_cast h2)
+  exact mod_cast h1.reduction (mod_cast h2)
 #align imo1981_q3.nat_predicate.reduction Imo1981Q3.NatPredicate.reduction
 
-theorem n_pos {m n : ℕ} (h1 : NatPredicate N m n) : 0 < n := by exact_mod_cast h1.n_range.left
+theorem n_pos {m n : ℕ} (h1 : NatPredicate N m n) : 0 < n := mod_cast h1.n_range.left
 #align imo1981_q3.nat_predicate.n_pos Imo1981Q3.NatPredicate.n_pos
 
-theorem m_pos {m n : ℕ} (h1 : NatPredicate N m n) : 0 < m := by exact_mod_cast h1.m_range.left
+theorem m_pos {m n : ℕ} (h1 : NatPredicate N m n) : 0 < m := mod_cast h1.m_range.left
 #align imo1981_q3.nat_predicate.m_pos Imo1981Q3.NatPredicate.m_pos
 
-theorem n_le_N {m n : ℕ} (h1 : NatPredicate N m n) : n ≤ N := by exact_mod_cast h1.n_range.right
+theorem n_le_N {m n : ℕ} (h1 : NatPredicate N m n) : n ≤ N := mod_cast h1.n_range.right
 set_option linter.uppercaseLean3 false in
 #align imo1981_q3.nat_predicate.n_le_N Imo1981Q3.NatPredicate.n_le_N
 

Archive/Imo/Imo1988Q6.lean

@@ -184,7 +184,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   · -- For the second condition, we note that it suffices to check that c ≠ m_x.
     suffices hc : c ≠ mx
     · refine' lt_of_le_of_ne _ hc
-      exact_mod_cast c_lt
+      exact mod_cast c_lt
     -- However, recall that B(m_x) ≠ m_x + m_y.
     -- If c = m_x, we can prove B(m_x) = m_x + m_y.
     contrapose! hm_B₂
@@ -237,14 +237,14 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
     · have hpos : z * z + x * x > 0 := by
         apply add_pos_of_nonneg_of_pos
         · apply mul_self_nonneg
-        · apply mul_pos <;> exact_mod_cast hx
+        · apply mul_pos <;> exact mod_cast hx
       have hzx : z * z + x * x = (z * x + 1) * k := by
         rw [← sub_eq_zero, ← h_root]
         ring
       rw [hzx] at hpos
       replace hpos : z * x + 1 > 0 := pos_of_mul_pos_left hpos (Int.ofNat_zero_le k)
       replace hpos : z * x ≥ 0 := Int.le_of_lt_add_one hpos
-      apply nonneg_of_mul_nonneg_left hpos (by exact_mod_cast hx)
+      apply nonneg_of_mul_nonneg_left hpos (mod_cast hx)
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt
       calc
@@ -284,7 +284,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
   · -- Show the descent step.
     intro x y _ hx h_base _ z _ _ hV₀
     constructor
-    · have zy_pos : z * y ≥ 0 := by rw [hV₀]; exact_mod_cast Nat.zero_le _
+    · have zy_pos : z * y ≥ 0 := by rw [hV₀]; exact mod_cast Nat.zero_le _
       apply nonneg_of_mul_nonneg_left zy_pos
       linarith
     · contrapose! hV₀ with x_lt_z

Archive/Imo/Imo2013Q5.lean

@@ -54,7 +54,7 @@ theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
       _ = x ^ n - y ^ n := geom_sum₂_mul x y n
   -- Choose n larger than 1 / (x - y).
   obtain ⟨N, hN⟩ := exists_nat_gt (1 / (x - y))
-  have hNp : 0 < N := by exact_mod_cast (one_div_pos.mpr hxmy).trans hN
+  have hNp : 0 < N := mod_cast (one_div_pos.mpr hxmy).trans hN
   have :=
     calc
       1 = (x - y) * (1 / (x - y)) := by field_simp
@@ -113,7 +113,7 @@ theorem fx_gt_xm1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 ≤ x)
     (x - 1 : ℝ) < f x := by
   have hx0 :=
     calc
-      (x - 1 : ℝ) < ⌊x⌋₊ := by exact_mod_cast Nat.sub_one_lt_floor x
+      (x - 1 : ℝ) < ⌊x⌋₊ := mod_cast Nat.sub_one_lt_floor x
       _ ≤ f ⌊x⌋₊ := H4 _ (Nat.floor_pos.2 hx)
   obtain h_eq | h_lt := (Nat.floor_le <| zero_le_one.trans hx).eq_or_lt
   · rwa [h_eq] at hx0
@@ -143,12 +143,12 @@ theorem fixed_point_of_pos_nat_pow {f : ℚ → ℝ} {n : ℕ} (hn : 0 < n)
     (H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y) (H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n)
     (H5 : ∀ x : ℚ, 1 < x → (x : ℝ) ≤ f x) {a : ℚ} (ha1 : 1 < a) (hae : f a = a) :
     f (a ^ n) = a ^ n := by
-  have hh0 : (a : ℝ) ^ n ≤ f (a ^ n) := by exact_mod_cast H5 (a ^ n) (one_lt_pow ha1 hn.ne')
+  have hh0 : (a : ℝ) ^ n ≤ f (a ^ n) := mod_cast H5 (a ^ n) (one_lt_pow ha1 hn.ne')
   have hh1 :=
     calc
       f (a ^ n) ≤ f a ^ n := pow_f_le_f_pow hn ha1 H1 H4
       _ = (a : ℝ) ^ n := by rw [← hae]
-  exact_mod_cast hh1.antisymm hh0
+  exact mod_cast hh1.antisymm hh0
 #align imo2013_q5.fixed_point_of_pos_nat_pow Imo2013Q5.fixed_point_of_pos_nat_pow
 
 theorem fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
@@ -170,7 +170,7 @@ theorem fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
       _ = f (a ^ N) := by ring_nf
       _ = a ^ N := (fixed_point_of_pos_nat_pow hNp H1 H4 H5 ha1 hae)
       _ = x + (a ^ N - x) := by ring
-  have heq := h1.antisymm (by exact_mod_cast h2)
+  have heq := h1.antisymm (mod_cast h2)
   linarith [H5 x hx, H5 _ h_big_enough]
 #align imo2013_q5.fixed_point_of_gt_1 Imo2013Q5.fixed_point_of_gt_1
 
@@ -191,7 +191,7 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
     calc
       ↑(pn + 2) * f x = (↑pn + 1 + 1) * f x := by norm_cast
       _ = (↑pn + 1) * f x + f x := by ring
-      _ ≤ f (↑pn.succ * x) + f x := by exact_mod_cast add_le_add_right (hpn pn.succ_pos) (f x)
+      _ ≤ f (↑pn.succ * x) + f x := mod_cast add_le_add_right (hpn pn.succ_pos) (f x)
       _ ≤ f ((↑pn + 1) * x + x) := by exact_mod_cast H2 _ _ (mul_pos pn.cast_add_one_pos hx) hx
       _ = f ((↑pn + 1 + 1) * x) := by ring_nf
       _ = f (↑(pn + 2) * x) := by norm_cast
@@ -216,10 +216,10 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
     have hxnm1 : ∀ n : ℕ, 0 < n → (x : ℝ) ^ n - 1 < f x ^ n := by
       intro n hn
       calc
-        (x : ℝ) ^ n - 1 < f (x ^ n) := by
-          exact_mod_cast fx_gt_xm1 (one_le_pow_of_one_le hx.le n) H1 H2 H4
+        (x : ℝ) ^ n - 1 < f (x ^ n) :=
+            mod_cast fx_gt_xm1 (one_le_pow_of_one_le hx.le n) H1 H2 H4
         _ ≤ f x ^ n := pow_f_le_f_pow hn hx H1 H4
-    have hx' : 1 < (x : ℝ) := by exact_mod_cast hx
+    have hx' : 1 < (x : ℝ) := mod_cast hx
     have hxp : 0 < x := by positivity
     exact le_of_all_pow_lt_succ' hx' (f_pos_of_pos hxp H1 H4) hxnm1
   have h_f_commutes_with_pos_nat_mul : ∀ n : ℕ, 0 < n → ∀ x : ℚ, 0 < x → f (n * x) = n * f x := by

Archive/Sensitivity.lean

@@ -353,7 +353,7 @@ theorem g_injective : Injective (g m) := by
 
 theorem f_image_g (w : V m.succ) (hv : ∃ v, g m v = w) : f m.succ w = √ (m + 1) • w := by
   rcases hv with ⟨v, rfl⟩
-  have : √ (m + 1) * √ (m + 1) = m + 1 := Real.mul_self_sqrt (by exact_mod_cast zero_le _)
+  have : √ (m + 1) * √ (m + 1) = m + 1 := Real.mul_self_sqrt (mod_cast zero_le _)
   rw [f_succ_apply, g_apply]
   simp [this, f_squared, smul_add, add_smul, smul_smul, V]
   abel
@@ -400,7 +400,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
   let W := Span (e '' H)
   let img := range (g m)
   suffices 0 < dim (W ⊓ img) by
-    exact_mod_cast exists_mem_ne_zero_of_rank_pos this
+    exact mod_cast exists_mem_ne_zero_of_rank_pos this
   have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1 : Cardinal) := by
     convert ← rank_submodule_le (W ⊔ img)
     rw [← Nat.cast_succ]

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -87,7 +87,7 @@ theorem irreducible_Phi (p : ℕ) (hp : p.Prime) (hpa : p ∣ a) (hpb : p ∣ b)
   apply irreducible_of_eisenstein_criterion
   · rwa [span_singleton_prime (Int.coe_nat_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
+    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
@@ -130,7 +130,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
     obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Ico' hle (hc _) (Set.mem_Ioc.mpr ⟨hf1, hf0⟩)
     obtain ⟨y, ⟨hy1, -⟩, hy2⟩ := intermediate_value_Ioc ha (hc _) (Set.mem_Ioc.mpr ⟨hf1, hfa⟩)
     exact ⟨x, y, (hx1.trans hy1).ne, hx2, hy2⟩
-  · replace hb : (b : ℝ) = a - 1 := by linarith [show (b : ℝ) + 1 ≤ a by exact_mod_cast hab]
+  · replace hb : (b : ℝ) = a - 1 := by linarith [show (b : ℝ) + 1 ≤ a from mod_cast hab]
     have hf1 : f 1 = 0 := by simp [hf, hb]
     have hfa :=
       calc

Archive/Wiedijk100Theorems/Partition.lean

@@ -521,14 +521,14 @@ theorem same_coeffs [Field α] (m n : ℕ) (h : n ≤ m) :
   rw [← same_gf, coeff_mul_prod_one_sub_of_lt_order]
   rintro i -
   rw [order_X_pow]
-  exact_mod_cast Nat.lt_succ_of_le (le_add_right h)
+  exact mod_cast Nat.lt_succ_of_le (le_add_right h)
 #align theorems_100.same_coeffs Theorems100.same_coeffs
 
 theorem partition_theorem (n : ℕ) :
     (Nat.Partition.odds n).card = (Nat.Partition.distincts n).card := by
   -- We need the counts to live in some field (which contains ℕ), so let's just use ℚ
-  suffices ((Nat.Partition.odds n).card : ℚ) = (Nat.Partition.distincts n).card by
-    exact_mod_cast this
+  suffices ((Nat.Partition.odds n).card : ℚ) = (Nat.Partition.distincts n).card from
+    mod_cast this
   rw [distinctGF_prop n (n + 1) (by linarith)]
   rw [oddGF_prop n (n + 1) (by linarith)]
   apply same_coeffs (n + 1) n n.le_succ

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -239,7 +239,7 @@ theorem Real.tendsto_sum_one_div_prime_atTop :
       _ = x / 2 := mul_one_div (x : ℝ) 2
   have h4 :=
     calc
-      (card M' : ℝ) ≤ 2 ^ k * x.sqrt := by exact_mod_cast card_le_two_pow_mul_sqrt
+      (card M' : ℝ) ≤ 2 ^ k * x.sqrt := by exact mod_cast card_le_two_pow_mul_sqrt
       _ = 2 ^ k * (2 ^ (k + 1) : ℕ) := by rw [Nat.sqrt_eq]
       _ = x / 2 := by field_simp [mul_right_comm, ← pow_succ']
   refine' lt_irrefl (x : ℝ) _

Mathlib/Algebra/CharP/CharAndCard.lean

@@ -61,8 +61,8 @@ theorem prime_dvd_char_iff_dvd_card {R : Type*} [CommRing R] [Fintype R] (p : 
     ⟨fun h =>
       h.trans <|
         Int.coe_nat_dvd.mp <|
-          (CharP.int_cast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <| by
-            exact_mod_cast CharP.cast_card_eq_zero R,
+          (CharP.int_cast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <|
+            mod_cast CharP.cast_card_eq_zero R,
       fun h => _⟩
   by_contra h₀
   rcases exists_prime_addOrderOf_dvd_card p h with ⟨r, hr⟩

Mathlib/Algebra/CharP/Invertible.lean

@@ -63,11 +63,11 @@ number when you need its inverse.
 
 
 instance invertibleTwo : Invertible (2 : K) :=
-  invertibleOfNonzero (by exact_mod_cast (by decide : 2 ≠ 0))
+  invertibleOfNonzero (mod_cast (by decide : 2 ≠ 0))
 #align invertible_two invertibleTwo
 
 instance invertibleThree : Invertible (3 : K) :=
-  invertibleOfNonzero (by exact_mod_cast (by decide : 3 ≠ 0))
+  invertibleOfNonzero (mod_cast (by decide : 3 ≠ 0))
 #align invertible_three invertibleThree
 
 end DivisionRing

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -108,7 +108,7 @@ theorem eq_neg_self_iff {a : R} : a = -a ↔ a = 0 :=
 
 theorem nat_mul_inj {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) : n = 0 ∨ a = b := by
   rw [← sub_eq_zero, ← mul_sub, mul_eq_zero, sub_eq_zero] at h
-  exact_mod_cast h
+  exact mod_cast h
 #align nat_mul_inj nat_mul_inj
 
 theorem nat_mul_inj' {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) (w : n ≠ 0) : a = b := by
@@ -121,7 +121,7 @@ theorem bit0_injective : Function.Injective (bit0 : R → R) := fun a b h => by
   dsimp [bit0] at h
   simp only [(two_mul a).symm, (two_mul b).symm] at h
   refine' nat_mul_inj' _ two_ne_zero
-  exact_mod_cast h
+  exact mod_cast h
 #align bit0_injective bit0_injective
 
 theorem bit1_injective : Function.Injective (bit1 : R → R) := fun a b h => by

Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

@@ -109,7 +109,7 @@ theorem of_convergence_epsilon :
   · have : v = g.convergents n := of_correctness_of_terminatedAt terminated_at_n
     have : v - g.convergents n = 0 := sub_eq_zero.mpr this
     rw [this]
-    exact_mod_cast ε_pos
+    exact mod_cast ε_pos
   · let B := g.denominators n
     let nB := g.denominators (n + 1)
     have abs_v_sub_conv_le : |v - g.convergents n| ≤ 1 / (B * nB) :=
@@ -122,28 +122,28 @@ theorem of_convergence_epsilon :
     have B_ineq : (fib (n + 1) : K) ≤ B :=
       haveI : ¬g.TerminatedAt (n - 1) := mt (terminated_stable n.pred_le) not_terminated_at_n
       succ_nth_fib_le_of_nth_denom (Or.inr this)
-    have zero_lt_B : 0 < B := B_ineq.trans_lt' $ by exact_mod_cast fib_pos.2 n.succ_pos
-    have nB_pos : 0 < nB := nB_ineq.trans_lt' $ by exact_mod_cast fib_pos.2 $ succ_pos _
+    have zero_lt_B : 0 < B := B_ineq.trans_lt' $ mod_cast fib_pos.2 n.succ_pos
+    have nB_pos : 0 < nB := nB_ineq.trans_lt' $ mod_cast fib_pos.2 $ succ_pos _
     have zero_lt_mul_conts : 0 < B * nB := by positivity
     suffices : 1 < ε * (B * nB); exact (div_lt_iff zero_lt_mul_conts).mpr this
     -- use that `N ≥ n` was obtained from the archimedean property to show the following
     have one_lt_ε_mul_N : 1 < ε * n := by
       have one_lt_ε_mul_N' : 1 < ε * (N' : K) := (div_lt_iff' ε_pos).mp one_div_ε_lt_N'
-      have : (N' : K) ≤ N := by exact_mod_cast le_max_left _ _
+      have : (N' : K) ≤ N := mod_cast le_max_left _ _
       have : ε * N' ≤ ε * n :=
-        (mul_le_mul_left ε_pos).mpr (le_trans this (by exact_mod_cast n_ge_N))
+        (mul_le_mul_left ε_pos).mpr (le_trans this (mod_cast n_ge_N))
       exact lt_of_lt_of_le one_lt_ε_mul_N' this
     suffices : ε * n ≤ ε * (B * nB); exact lt_of_lt_of_le one_lt_ε_mul_N this
     -- cancel `ε`
     suffices : (n : K) ≤ B * nB;
     exact (mul_le_mul_left ε_pos).mpr this
     show (n : K) ≤ B * nB
     calc
-      (n : K) ≤ fib n := by exact_mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
-      _ ≤ fib (n + 1) := by exact_mod_cast fib_le_fib_succ
-      _ ≤ fib (n + 1) * fib (n + 1) := by exact_mod_cast (fib (n + 1)).le_mul_self
+      (n : K) ≤ fib n := mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
+      _ ≤ fib (n + 1) := mod_cast fib_le_fib_succ
+      _ ≤ fib (n + 1) * fib (n + 1) := mod_cast (fib (n + 1)).le_mul_self
       _ ≤ fib (n + 1) * fib (n + 2) :=
-            mul_le_mul_of_nonneg_left (by exact_mod_cast fib_le_fib_succ) (cast_nonneg _)
+            mul_le_mul_of_nonneg_left (mod_cast fib_le_fib_succ) (cast_nonneg _)
       _ ≤ B * nB := mul_le_mul B_ineq nB_ineq (cast_nonneg _) zero_lt_B.le
 #align generalized_continued_fraction.of_convergence_epsilon GeneralizedContinuedFraction.of_convergence_epsilon
 

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -143,7 +143,7 @@ theorem of_one_le_get?_part_denom {b : K}
     ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b
   exact IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
   rw [← ifp_n_b_eq_gp_n_b]
-  exact_mod_cast IntFractPair.one_le_succ_nth_stream_b succ_nth_stream_eq
+  exact mod_cast IntFractPair.one_le_succ_nth_stream_b succ_nth_stream_eq
 #align generalized_continued_fraction.of_one_le_nth_part_denom GeneralizedContinuedFraction.of_one_le_get?_part_denom
 
 /--
@@ -225,7 +225,7 @@ theorem fib_le_of_continuantsAux_b :
         suffices 1 * (fib (n + 1) : K) ≤ gp.b * pconts.b by rwa [one_mul] at this
         have one_le_gp_b : (1 : K) ≤ gp.b :=
           of_one_le_get?_part_denom (part_denom_eq_s_b s_ppred_nth_eq)
-        have : (0 : K) ≤ fib (n + 1) := by exact_mod_cast (fib (n + 1)).zero_le
+        have : (0 : K) ≤ fib (n + 1) := mod_cast (fib (n + 1)).zero_le
         have : (0 : K) ≤ gp.b := le_trans zero_le_one one_le_gp_b
         mono
         · norm_num
@@ -261,7 +261,7 @@ theorem zero_le_of_continuantsAux_b : 0 ≤ ((of v).continuantsAux n).b := by
         simp only [this, IH]
     · -- non-terminating case
       calc
-        (0 : K) ≤ fib (n + 1) := by exact_mod_cast (n + 1).fib.zero_le
+        (0 : K) ≤ fib (n + 1) := mod_cast (n + 1).fib.zero_le
         _ ≤ ((of v).continuantsAux (n + 1)).b := fib_le_of_continuantsAux_b (Or.inr not_terminated)
 #align generalized_continued_fraction.zero_le_of_continuants_aux_b GeneralizedContinuedFraction.zero_le_of_continuantsAux_b
 
@@ -495,7 +495,7 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) :
     haveI : ¬g.TerminatedAt (n - 1) := mt (terminated_stable n.pred_le) not_terminated_at_n
     fib_le_of_continuantsAux_b <| Or.inr this
   have zero_lt_conts_b : 0 < conts.b :=
-    conts_b_ineq.trans_lt' $ by exact_mod_cast fib_pos.2 n.succ_pos
+    conts_b_ineq.trans_lt' $ mod_cast fib_pos.2 n.succ_pos
   -- `denom'` is positive, so we can remove `|⬝|` from our goal
   suffices 1 / denom' ≤ 1 / denom by
     have : |(-1) ^ n / denom'| = 1 / denom' := by
@@ -506,7 +506,7 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) :
             haveI : ¬g.TerminatedAt (n - 2) :=
               mt (terminated_stable (n.sub_le 2)) not_terminated_at_n
             fib_le_of_continuantsAux_b <| Or.inr this
-          le_trans (by exact_mod_cast (fib n).zero_le) this
+          le_trans (mod_cast (fib n).zero_le) this
         have : 0 < ifp_n.fr⁻¹ :=
           haveI zero_le_ifp_n_fract : 0 ≤ ifp_n.fr :=
             IntFractPair.nth_stream_fr_nonneg stream_nth_eq
@@ -518,7 +518,7 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) :
   suffices 0 < denom ∧ denom ≤ denom' from div_le_div_of_le_left zero_le_one this.left this.right
   constructor
   · have : 0 < pred_conts.b + gp.b * conts.b :=
-      nextConts_b_ineq.trans_lt' $ by exact_mod_cast fib_pos.2 $ succ_pos _
+      nextConts_b_ineq.trans_lt' $ mod_cast fib_pos.2 $ succ_pos _
     solve_by_elim [mul_pos]
   · -- we can cancel multiplication by `conts.b` and addition with `pred_conts.b`
     suffices : gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b

Mathlib/Algebra/GeomSum.lean

@@ -210,7 +210,7 @@ theorem sub_one_dvd_pow_sub_one [Ring α] (x : α) (n : ℕ) :
 theorem nat_sub_dvd_pow_sub_pow (x y n : ℕ) : x - y ∣ x ^ n - y ^ n := by
   cases' le_or_lt y x with h h
   · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_of_le_left h _
-    exact_mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
+    exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
   · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_of_le_left h.le _
     exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)
 #align nat_sub_dvd_pow_sub_pow nat_sub_dvd_pow_sub_pow
@@ -222,8 +222,8 @@ theorem Odd.add_dvd_pow_add_pow [CommRing α] (x y : α) {n : ℕ} (h : Odd n) :
   exact Dvd.intro_left _ h₁
 #align odd.add_dvd_pow_add_pow Odd.add_dvd_pow_add_pow
 
-theorem Odd.nat_add_dvd_pow_add_pow (x y : ℕ) {n : ℕ} (h : Odd n) : x + y ∣ x ^ n + y ^ n := by
-  exact_mod_cast Odd.add_dvd_pow_add_pow (x : ℤ) (↑y) h
+theorem Odd.nat_add_dvd_pow_add_pow (x y : ℕ) {n : ℕ} (h : Odd n) : x + y ∣ x ^ n + y ^ n :=
+  mod_cast Odd.add_dvd_pow_add_pow (x : ℤ) (↑y) h
 #align odd.nat_add_dvd_pow_add_pow Odd.nat_add_dvd_pow_add_pow
 
 theorem geom_sum_mul [Ring α] (x : α) (n : ℕ) : (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1 := by

Mathlib/Algebra/LinearRecurrence.lean

@@ -102,7 +102,7 @@ theorem eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : Fin E.order → α}
   intro n
   rw [mkSol]
   split_ifs with h'
-  · exact_mod_cast heq ⟨n, h'⟩
+  · exact mod_cast heq ⟨n, h'⟩
   simp only
   rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]
   congr with k
@@ -163,7 +163,7 @@ theorem sol_eq_of_eq_init (u v : ℕ → α) (hu : E.IsSolution u) (hv : E.IsSol
   suffices h' : u' = v'; exact h' ▸ rfl
   rw [← E.toInit.toEquiv.apply_eq_iff_eq, LinearEquiv.coe_toEquiv]
   ext x
-  exact_mod_cast h (mem_range.mpr x.2)
+  exact mod_cast h (mem_range.mpr x.2)
 #align linear_recurrence.sol_eq_of_eq_init LinearRecurrence.sol_eq_of_eq_init
 
 /-! `E.tupleSucc` maps `![s₀, s₁, ..., sₙ]` to `![s₁, ..., sₙ, ∑ (E.coeffs i) * sᵢ]`,