fixes for leanprover/lean4#11004

Author: kim-em

Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

@@ -138,7 +138,8 @@ theorem abs_def (q : ℚ) : |q| = q.num.natAbs /. q.den := by
 theorem abs_def' (q : ℚ) :
     |q| = ⟨|q.num|, q.den, q.den_ne_zero, q.num.abs_eq_natAbs ▸ q.reduced⟩ := by
   refine ext ?_ ?_ <;>
-    simp [Int.abs_eq_natAbs, abs_def, ← Rat.mk_eq_divInt q.num.natAbs _ q.den_ne_zero q.reduced]
+    simp [Int.abs_eq_natAbs, abs_def,
+      ← Rat.mk_eq_divInt (num := q.num.natAbs) (nz := q.den_ne_zero) (c := q.reduced)]
 
 @[simp]
 theorem num_abs_eq_abs_num (q : ℚ) : |q|.num = |q.num| := by

Mathlib/Data/Rat/Lemmas.lean

@@ -245,13 +245,13 @@ theorem num_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAb
     (a / b : ℚ).num = a := by
   lift b to ℕ using hb0.le
   simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0
-  rw [← Rat.divInt_eq_div, ← mk_eq_divInt _ _ hb0.ne' h]
+  rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]
 
 theorem den_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) :
     ((a / b : ℚ).den : ℤ) = b := by
   lift b to ℕ using hb0.le
   simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0
-  rw [← Rat.divInt_eq_div, ← mk_eq_divInt _ _ hb0.ne' h]
+  rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]
 
 theorem div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprime a.natAbs b.natAbs)
     (h2 : Nat.Coprime c.natAbs d.natAbs) (h : (a : ℚ) / b = (c : ℚ) / d) : a = c ∧ b = d := by

Mathlib/Order/Fin/Basic.lean

@@ -185,8 +185,7 @@ lemma strictMono_addNat (m) : StrictMono ((addNat · m) : Fin n → Fin (n + m))
 
 lemma strictMono_succAbove (p : Fin (n + 1)) : StrictMono (succAbove p) :=
   strictMono_castSucc.ite strictMono_succ
-    (fun _ _ hij hj => (castSucc_lt_castSucc_iff.mpr hij).trans hj) fun i =>
-    (castSucc_lt_succ i).le
+    (fun _ _ hij hj => (castSucc_lt_castSucc_iff.mpr hij).trans hj) fun _ => castSucc_lt_succ.le
 
 variable {p : Fin (n + 1)} {i j : Fin n}