chore: prepare for the next lean version bump (#24449)

Author: Ruben-VandeVelde

Archive/Imo/Imo1998Q2.lean

@@ -174,9 +174,9 @@ theorem judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1)
   let y := (Finset.univ.filter fun j => ¬r c j).card
   have h : (Finset.univ.filter fun p : JudgePair J => p.Agree r c).card = x * x + y * y := by
     simp [x, y, ← Finset.filter_product_card]
-  rw [h]; apply Int.le_of_ofNat_le_ofNat; simp only [Int.ofNat_add, Int.ofNat_mul]
+  rw [h]; apply Int.le_of_ofNat_le_ofNat; simp only [Int.natCast_add, Int.natCast_mul]
   apply norm_bound_of_odd_sum
-  suffices x + y = 2 * z + 1 by simp [← Int.ofNat_add, this]
+  suffices x + y = 2 * z + 1 by simp [← Int.natCast_add, this]
   rw [Finset.filter_card_add_filter_neg_card_eq_card, ← hJ, Finset.card_univ]
 
 open scoped Classical in

Archive/Imo/Imo2008Q3.lean

@@ -40,7 +40,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   let n := Int.natAbs m
   have hnat₁ : p ∣ n ^ 2 + 1 := by
     refine Int.natCast_dvd_natCast.mp ?_
-    simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
+    simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.natCast_succ, Int.natCast_dvd_natCast.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 neg_add_cancel 1

Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

@@ -276,7 +276,7 @@ theorem stream_nth_fr_num_le_fr_num_sub_n_rat :
   | succ n IH =>
     intro ifp_succ_n stream_succ_nth_eq
     suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by
-      rw [Int.ofNat_succ, sub_add_eq_sub_sub]
+      rw [Int.natCast_succ, sub_add_eq_sub_sub]
       solve_by_elim [le_sub_right_of_add_le]
     rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
     have : ifp_succ_n.fr.num < ifp_n.fr.num :=

Mathlib/Algebra/GCDMonoid/Nat.lean

@@ -104,7 +104,7 @@ instance : GCDMonoid ℤ where
   gcd_dvd_right _ _ := Int.gcd_dvd_right
   dvd_gcd := dvd_coe_gcd
   gcd_mul_lcm a b := by
-    rw [← Int.ofNat_mul, gcd_mul_lcm, natCast_natAbs, abs_eq_normalize]
+    rw [← Int.natCast_mul, gcd_mul_lcm, natCast_natAbs, abs_eq_normalize]
     exact normalize_associated (a * b)
   lcm_zero_left _ := natCast_eq_zero.2 <| Nat.lcm_zero_left _
   lcm_zero_right _ := natCast_eq_zero.2 <| Nat.lcm_zero_right _

Mathlib/Algebra/Group/Basic.lean

@@ -818,7 +818,7 @@ theorem inv_pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^
 
 @[to_additive add_one_zsmul]
 lemma zpow_add_one (a : G) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
-  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_natCast, pow_succ]
+  | (n : ℕ) => by simp only [← Int.natCast_succ, zpow_natCast, pow_succ]
   | -1 => by simp [Int.add_left_neg]
   | .negSucc (n + 1) => by
     rw [zpow_negSucc, pow_succ', mul_inv_rev, inv_mul_cancel_right]

Mathlib/Algebra/Group/Int/Defs.lean

@@ -44,8 +44,8 @@ instance instAddCommGroup : AddCommGroup ℤ where
   zsmul := (·*·)
   zsmul_zero' := Int.zero_mul
   zsmul_succ' m n := by
-    simp only [ofNat_succ, Int.add_mul, Int.add_comm, Int.one_mul]
-  zsmul_neg' m n := by simp only [negSucc_eq, ofNat_succ, Int.neg_mul]
+    simp only [Int.natCast_succ, Int.add_mul, Int.add_comm, Int.one_mul]
+  zsmul_neg' m n := by simp only [negSucc_eq, Int.natCast_succ, Int.neg_mul]
   sub_eq_add_neg _ _ := Int.sub_eq_add_neg
 
 /-!

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -63,7 +63,7 @@ instance instOne : One (WithOne α) :=
 
 @[to_additive]
 instance instMul [Mul α] : Mul (WithOne α) :=
-  ⟨Option.liftOrGet (· * ·)⟩
+  ⟨Option.merge (· * ·)⟩
 
 @[to_additive]
 instance instInv [Inv α] : Inv (WithOne α) :=
@@ -155,8 +155,8 @@ protected theorem cases_on {P : WithOne α → Prop} : ∀ x : WithOne α, P 1 
 instance instMulOneClass [Mul α] : MulOneClass (WithOne α) where
   mul := (· * ·)
   one := 1
-  one_mul := (Option.liftOrGet_isId _).left_id
-  mul_one := (Option.liftOrGet_isId _).right_id
+  one_mul := (Option.lawfulIdentity_merge _).left_id
+  mul_one := (Option.lawfulIdentity_merge _).right_id
 
 @[to_additive (attr := simp, norm_cast)]
 lemma coe_mul [Mul α] (a b : α) : (↑(a * b) : WithOne α) = a * b := rfl

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -406,12 +406,12 @@ lemma zero_zpow_eq_one₀ {n : ℤ} : (0 : G₀) ^ n = 1 ↔ n = 0 := by
   rw [zero_zpow_eq, one_ne_zero.ite_eq_left_iff]
 
 lemma zpow_add_one₀ (ha : a ≠ 0) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
-  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_natCast, pow_succ]
+  | (n : ℕ) => by simp only [← Int.natCast_succ, zpow_natCast, pow_succ]
   | -1 => by simp [ha]
   | .negSucc (n + 1) => by
-    rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg, ← Int.ofNat_succ,
-      zpow_natCast, zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel₀ ha,
-      mul_one]
+    rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg,
+      ← Int.natCast_succ, zpow_natCast, zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc,
+      inv_mul_cancel₀ ha, mul_one]
 
 lemma zpow_sub_one₀ (ha : a ≠ 0) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
   calc

Mathlib/Algebra/Homology/Embedding/Connect.lean

@@ -90,7 +90,7 @@ lemma d_comp_d (n m p : ℤ) : h.d n m ≫ h.d m p = 0 := by
   obtain n | (_ | _ | n) := n
   · obtain rfl : m = .ofNat (n + 1) := by simp [← hnm]
     obtain rfl : p = .ofNat (n + 2) := by simp [← hmp]; omega
-    simp
+    simp only [Int.ofNat_eq_coe, X_ofNat, d_ofNat, HomologicalComplex.d_comp_d]
   · obtain rfl : m = 0 := by omega
     obtain rfl : p = 1 := by omega
     simp

Mathlib/Algebra/Polynomial/Laurent.lean

@@ -345,11 +345,11 @@ theorem exists_T_pow (f : R[T;T⁻¹]) : ∃ (n : ℕ) (f' : R[X]), toLaurent f'
   · rintro f g ⟨m, fn, hf⟩ ⟨n, gn, hg⟩
     refine ⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩
     simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow,
-      mul_T_assoc, Int.ofNat_add]
+      mul_T_assoc, Int.natCast_add]
   · rcases n with n | n
     · exact ⟨0, Polynomial.C a * X ^ n, by simp⟩
     · refine ⟨n + 1, Polynomial.C a, ?_⟩
-      simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.ofNat_succ, mul_T_assoc,
+      simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.natCast_succ, mul_T_assoc,
         neg_add_cancel, T_zero, mul_one]
 
 /-- This is a version of `exists_T_pow` stated as an induction principle. -/