fix: patch for std4#198 (more mul lemmas for Nat) (#6204)

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

Mathlib/Algebra/EuclideanDomain/Instances.lean

@@ -33,7 +33,7 @@ instance Int.euclideanDomain : EuclideanDomain ℤ :=
       not_lt_of_ge <| by
         rw [← mul_one a.natAbs, Int.natAbs_mul]
         rw [← Int.natAbs_pos] at b0
-        exact Nat.mul_le_mul_of_nonneg_left b0 }
+        exact Nat.mul_le_mul_left _ b0 }
 
 -- see Note [lower instance priority]
 instance (priority := 100) Field.toEuclideanDomain {K : Type*} [Field K] : EuclideanDomain K :=

Mathlib/CategoryTheory/EqToHom.lean

@@ -107,7 +107,7 @@ theorem congrArg_cast_hom_left {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :
   cases p
   simp
 
- /-- If we (perhaps unintentionally) perform equational rewriting on
+/-- If we (perhaps unintentionally) perform equational rewriting on
 the source object of a morphism,
 we can replace the resulting `_.mpr f` term by a composition with an `eqToHom`.
 

Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -42,7 +42,8 @@ def stepBound (n : ℕ) : ℕ :=
   n * 4 ^ n
 #align szemeredi_regularity.step_bound SzemerediRegularity.stepBound
 
-theorem le_stepBound : id ≤ stepBound := fun n => Nat.le_mul_of_pos_right <| pow_pos (by norm_num) n
+theorem le_stepBound : id ≤ stepBound := fun n =>
+  Nat.le_mul_of_pos_right _ <| pow_pos (by norm_num) n
 #align szemeredi_regularity.le_step_bound SzemerediRegularity.le_stepBound
 
 theorem stepBound_mono : Monotone stepBound := fun a b h =>
@@ -214,7 +215,7 @@ noncomputable def bound : ℕ :=
 #align szemeredi_regularity.bound SzemerediRegularity.bound
 
 theorem initialBound_le_bound : initialBound ε l ≤ bound ε l :=
-  (id_le_iterate_of_id_le le_stepBound _ _).trans <| Nat.le_mul_of_pos_right <| by positivity
+  (id_le_iterate_of_id_le le_stepBound _ _).trans <| Nat.le_mul_of_pos_right _ <| by positivity
 #align szemeredi_regularity.initial_bound_le_bound SzemerediRegularity.initialBound_le_bound
 
 theorem le_bound : l ≤ bound ε l :=

Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean

@@ -68,10 +68,11 @@ theorem equitabilise_aux (hs : a * m + b * (m + 1) = s.card) :
       ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = s.card - n := by
     rw [hn, ← hs]
     split_ifs with h <;> rw [tsub_mul, one_mul]
-    · refine' ⟨m_pos, le_succ _, le_add_right (le_mul_of_pos_left ‹0 < a›), _⟩
-      rw [tsub_add_eq_add_tsub (le_mul_of_pos_left h)]
-    · refine' ⟨succ_pos', le_rfl, le_add_left (le_mul_of_pos_left <| hab.resolve_left ‹¬0 < a›), _⟩
-      rw [← add_tsub_assoc_of_le (le_mul_of_pos_left <| hab.resolve_left ‹¬0 < a›)]
+    · refine' ⟨m_pos, le_succ _, le_add_right (Nat.le_mul_of_pos_left _ ‹0 < a›), _⟩
+      rw [tsub_add_eq_add_tsub (Nat.le_mul_of_pos_left _ h)]
+    · refine' ⟨succ_pos', le_rfl,
+        le_add_left (Nat.le_mul_of_pos_left _ <| hab.resolve_left ‹¬0 < a›), _⟩
+      rw [← add_tsub_assoc_of_le (Nat.le_mul_of_pos_left _ <| hab.resolve_left ‹¬0 < a›)]
   /- We will call the inductive hypothesis on a partition of `s \ t` for a carefully chosen `t ⊆ s`.
     To decide which, however, we must distinguish the case where all parts of `P` have size `m` (in
     which case we take `t` to be an arbitrary subset of `s` of size `n`) from the case where at

Mathlib/Data/FP/Basic.lean

@@ -97,7 +97,7 @@ theorem Float.Zero.valid : ValidFinite emin 0 :=
       ring_nf
       rw [mul_comm]
       assumption
-    le_trans C.precMax (Nat.le_mul_of_pos_left (by decide)),
+    le_trans C.precMax (Nat.le_mul_of_pos_left _ two_pos),
     by (rw [max_eq_right]; simp [sub_eq_add_neg])⟩
 #align fp.float.zero.valid FP.Float.Zero.valid
 

Mathlib/Data/List/Rotate.lean

@@ -445,7 +445,7 @@ theorem IsRotated.symm (h : l ~r l') : l' ~r l := by
   · exists 0
   · use (hd :: tl).length * n - n
     rw [rotate_rotate, add_tsub_cancel_of_le, rotate_length_mul]
-    exact Nat.le_mul_of_pos_left (by simp)
+    exact Nat.le_mul_of_pos_left _ (by simp)
 #align list.is_rotated.symm List.IsRotated.symm
 
 theorem isRotated_comm : l ~r l' ↔ l' ~r l :=

Mathlib/Data/Nat/Choose/Central.lean

@@ -40,7 +40,7 @@ theorem centralBinom_eq_two_mul_choose (n : ℕ) : centralBinom n = (2 * n).choo
 #align nat.central_binom_eq_two_mul_choose Nat.centralBinom_eq_two_mul_choose
 
 theorem centralBinom_pos (n : ℕ) : 0 < centralBinom n :=
-  choose_pos (Nat.le_mul_of_pos_left zero_lt_two)
+  choose_pos (Nat.le_mul_of_pos_left _ zero_lt_two)
 #align nat.central_binom_pos Nat.centralBinom_pos
 
 theorem centralBinom_ne_zero (n : ℕ) : centralBinom n ≠ 0 :=
@@ -62,7 +62,7 @@ theorem choose_le_centralBinom (r n : ℕ) : choose (2 * n) r ≤ centralBinom n
 
 theorem two_le_centralBinom (n : ℕ) (n_pos : 0 < n) : 2 ≤ centralBinom n :=
   calc
-    2 ≤ 2 * n := le_mul_of_pos_right n_pos
+    2 ≤ 2 * n := Nat.le_mul_of_pos_right _ n_pos
     _ = (2 * n).choose 1 := (choose_one_right (2 * n)).symm
     _ ≤ centralBinom n := choose_le_centralBinom 1 n
 #align nat.two_le_central_binom Nat.two_le_centralBinom
@@ -112,7 +112,7 @@ theorem four_pow_le_two_mul_self_mul_centralBinom :
     calc
       4 ^ (n+4) ≤ (n+4) * centralBinom (n+4) := (four_pow_lt_mul_centralBinom _ le_add_self).le
       _ ≤ 2 * (n+4) * centralBinom (n+4) := by
-        rw [mul_assoc]; refine' le_mul_of_pos_left zero_lt_two
+        rw [mul_assoc]; refine' Nat.le_mul_of_pos_left _ zero_lt_two
 #align nat.four_pow_le_two_mul_self_mul_central_binom Nat.four_pow_le_two_mul_self_mul_centralBinom
 
 theorem two_dvd_centralBinom_succ (n : ℕ) : 2 ∣ centralBinom (n + 1) := by

Mathlib/Data/Nat/Defs.lean

@@ -277,8 +277,8 @@ lemma one_lt_mul_iff : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n) := by
     · simp at h
     · exact Nat.not_lt_of_le (Nat.mul_le_mul h'.1 h'.2) h
   · obtain hm | hn := h.2.2
-    · exact Nat.mul_lt_mul hm h.2.1 Nat.zero_lt_one
-    · exact Nat.mul_lt_mul' h.1 hn h.1
+    · exact Nat.mul_lt_mul_of_lt_of_le' hm h.2.1 Nat.zero_lt_one
+    · exact Nat.mul_lt_mul_of_le_of_lt h.1 hn h.1
 
 /-! ### `div` -/
 

Mathlib/Data/Nat/Factorial/Basic.lean

@@ -306,7 +306,7 @@ theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, n ^ k ≤ n.ascFactori
 
 theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2) := by
   rw [pow_succ, ascFactorial, mul_comm]
-  exact Nat.mul_lt_mul (lt_add_of_pos_right (n + 1) (succ_pos k))
+  exact Nat.mul_lt_mul_of_lt_of_le' (lt_add_of_pos_right (n + 1) (succ_pos k))
     (pow_succ_le_ascFactorial n.succ _) (NeZero.pos ((n + 1) ^ (k + 1)))
 #align nat.pow_lt_asc_factorial' Nat.pow_lt_ascFactorial'
 
@@ -320,7 +320,7 @@ theorem ascFactorial_le_pow_add (n : ℕ) : ∀ k : ℕ, (n+1).ascFactorial k 
   | 0 => by rw [ascFactorial_zero, pow_zero]
   | k + 1 => by
     rw [ascFactorial_succ, pow_succ, mul_comm, ← add_assoc, add_right_comm n 1 k]
-    exact Nat.mul_le_mul_of_nonneg_right
+    exact Nat.mul_le_mul_right _
       ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_of_le_left (le_succ _) _))
 #align nat.asc_factorial_le_pow_add Nat.ascFactorial_le_pow_add
 
@@ -329,7 +329,7 @@ theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1).a
   | 1 => by intro; contradiction
   | k + 2 => fun _ => by
     rw [pow_succ, mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]
-    exact Nat.mul_lt_mul' le_rfl ((ascFactorial_le_pow_add n _).trans_lt
+    exact Nat.mul_lt_mul_of_le_of_lt le_rfl ((ascFactorial_le_pow_add n _).trans_lt
       (pow_lt_pow_left (@lt_add_one ℕ _ _ _ _ _ _ _) (zero_le _) k.succ_ne_zero)) (succ_pos _)
 #align nat.asc_factorial_lt_pow_add Nat.ascFactorial_lt_pow_add
 
@@ -437,7 +437,7 @@ theorem pow_sub_le_descFactorial (n : ℕ) : ∀ k : ℕ, (n + 1 - k) ^ k ≤ n.
   | 0 => by rw [descFactorial_zero, pow_zero]
   | k + 1 => by
     rw [descFactorial_succ, pow_succ, succ_sub_succ, mul_comm]
-    apply Nat.mul_le_mul_of_nonneg_left
+    apply Nat.mul_le_mul_left
     exact   (le_trans (Nat.pow_le_pow_left (tsub_le_tsub_right (le_succ _) _) k)
           (pow_sub_le_descFactorial n k))
 #align nat.pow_sub_le_desc_factorial Nat.pow_sub_le_descFactorial
@@ -479,7 +479,7 @@ theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k 
   | 1 => by intro; contradiction
   | k + 2 => fun _ => by
     rw [descFactorial_succ, pow_succ', mul_comm, mul_comm n]
-    exact Nat.mul_lt_mul' (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ)
+    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ)
       (pow_pos (Nat.lt_of_succ_le hn) _)
 #align nat.desc_factorial_lt_pow Nat.descFactorial_lt_pow
 

Mathlib/Data/Nat/Factorial/DoubleFactorial.lean

@@ -57,7 +57,7 @@ theorem factorial_eq_mul_doubleFactorial : ∀ n : ℕ, (n + 1)! = (n + 1)‼ *
 lemma doubleFactorial_le_factorial : ∀ n, n‼ ≤ n !
   | 0 => le_rfl
   | n + 1 => by
-    rw [factorial_eq_mul_doubleFactorial]; exact le_mul_of_pos_right n.doubleFactorial_pos
+    rw [factorial_eq_mul_doubleFactorial]; exact Nat.le_mul_of_pos_right _ n.doubleFactorial_pos
 
 theorem doubleFactorial_two_mul : ∀ n : ℕ, (2 * n)‼ = 2 ^ n * n !
   | 0 => rfl

Mathlib/Data/Nat/Fib/Basic.lean

@@ -193,7 +193,7 @@ theorem fib_two_mul_add_two (n : ℕ) :
   rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]
   -- porting note: A bunch of issues similar to [this zulip thread](https://github.com/leanprover-community/mathlib4/pull/1576) with `zify`
   have : fib n ≤ 2 * fib (n + 1) :=
-    le_trans (fib_le_fib_succ) (mul_comm 2 _ ▸ le_mul_of_pos_right two_pos)
+    le_trans (fib_le_fib_succ) (mul_comm 2 _ ▸ Nat.le_mul_of_pos_right _ two_pos)
   zify [this]
   ring
 

Mathlib/Data/Nat/Order/Basic.lean

@@ -275,18 +275,10 @@ theorem le_mul_self : ∀ n : ℕ, n ≤ n * n
   | n + 1 => by simp
 #align nat.le_mul_self Nat.le_mul_self
 
-theorem le_mul_of_pos_left (h : 0 < n) : m ≤ n * m := by
-  conv =>
-    lhs
-    rw [← one_mul m]
-  exact mul_le_mul_of_nonneg_right h.nat_succ_le (zero_le _)
+-- Moved to Std
 #align nat.le_mul_of_pos_left Nat.le_mul_of_pos_left
 
-theorem le_mul_of_pos_right (h : 0 < n) : m ≤ m * n := by
-  conv =>
-    lhs
-    rw [← mul_one m]
-  exact mul_le_mul_of_nonneg_left h.nat_succ_le (zero_le _)
+-- Moved to Std
 #align nat.le_mul_of_pos_right Nat.le_mul_of_pos_right
 
 theorem mul_self_inj : m * m = n * n ↔ m = n :=
@@ -463,7 +455,7 @@ theorem not_dvd_of_pos_of_lt (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n := by
   rintro ⟨k, rfl⟩
   rcases Nat.eq_zero_or_pos k with (rfl | hk)
   · exact lt_irrefl 0 h1
-  · exact not_lt.2 (le_mul_of_pos_right hk) h2
+  · exact not_lt.2 (Nat.le_mul_of_pos_right _ hk) h2
 #align nat.not_dvd_of_pos_of_lt Nat.not_dvd_of_pos_of_lt
 
 /-- If `m` and `n` are equal mod `k`, `m - n` is zero mod `k`. -/

Mathlib/Data/Nat/Sqrt.lean

@@ -57,7 +57,7 @@ private theorem sqrt_isSqrt (n : ℕ) : IsSqrt n (sqrt n) := by
     rw [lt_add_one_iff, add_assoc, ← mul_two]
     refine le_trans (div_add_mod' (n + 2) 2).ge ?_
     rw [add_comm, add_le_add_iff_right, add_mod_right]
-    simp only [zero_lt_two, add_div_right, succ_mul_succ_eq]
+    simp only [zero_lt_two, add_div_right, succ_mul_succ]
     refine le_trans (b := 1) ?_ ?_
     · exact (lt_succ.1 <| mod_lt n zero_lt_two)
     · simp only [le_add_iff_nonneg_left]; exact zero_le _

Mathlib/Data/ZMod/Basic.lean

@@ -1161,7 +1161,7 @@ theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (
   rw [← add_le_add_iff_right x.natAbs]
   refine' le_trans (le_trans ((add_le_add_iff_left _).2 hl) _) (Int.natAbs_sub_le _ _)
   rw [add_sub_cancel, Int.natAbs_mul, Int.natAbs_ofNat]
-  refine' le_trans _ (Nat.le_mul_of_pos_right <| Int.natAbs_pos.2 hm)
+  refine' le_trans _ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)
   rw [← mul_two]; apply Nat.div_mul_le_self
 #align zmod.nat_abs_min_of_le_div_two ZMod.natAbs_min_of_le_div_two
 

Mathlib/FieldTheory/SeparableDegree.lean

@@ -588,7 +588,7 @@ theorem finSepDegree_eq_finrank_of_isSeparable [IsSeparable F E] :
     rw [H L h] at hd
     by_cases hd' : finSepDegree L E = 0
     · rw [← hd, hd', mul_zero]
-    linarith only [h', hd, Nat.le_mul_of_pos_right (m := finrank F L) (Nat.pos_of_ne_zero hd')]
+    linarith only [h', hd, Nat.le_mul_of_pos_right (finrank F L) (Nat.pos_of_ne_zero hd')]
   rw [← finSepDegree_top F, ← finrank_top F E]
   refine induction_on_adjoin (fun K : IntermediateField F E ↦ finSepDegree F K = finrank F K)
     (by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot]) (fun L x h ↦ ?_) ⊤
@@ -608,7 +608,7 @@ theorem finSepDegree_eq_finrank_iff [FiniteDimensional F E] :
     have halg := IsAlgebraic.of_finite F x
     refine (finSepDegree_adjoin_simple_eq_finrank_iff F E x halg).1 <| le_antisymm
       (finSepDegree_adjoin_simple_le_finrank F E x halg) <| le_of_not_lt fun h ↦ ?_
-    have := Nat.mul_lt_mul h (finSepDegree_le_finrank F⟮x⟯ E) Fin.size_pos'
+    have := Nat.mul_lt_mul_of_lt_of_le' h (finSepDegree_le_finrank F⟮x⟯ E) Fin.size_pos'
     rw [finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E (Algebra.IsAlgebraic.of_finite _ E),
       FiniteDimensional.finrank_mul_finrank F F⟮x⟯ E] at this
     linarith only [heq, this]⟩, fun _ ↦ finSepDegree_eq_finrank_of_isSeparable F E⟩

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -462,7 +462,7 @@ Many lemmas are proven more generally in mathlib `algebra/order/sub` -/
 
 #align nat.mul_self_sub_mul_self_eq Nat.mul_self_sub_mul_self_eq
 
-#align nat.succ_mul_succ_eq Nat.succ_mul_succ_eq
+#align nat.succ_mul_succ_eq Nat.succ_mul_succ
 
 /-! min -/
 

Mathlib/Init/Logic.lean

@@ -38,8 +38,6 @@ set_option autoImplicit true
 /- Eq -/
 
 alias proof_irrel := proofIrrel
-alias congr_fun := congrFun
-alias congr_arg := congrArg
 
 @[deprecated] theorem trans_rel_left {α : Sort u} {a b c : α}
     (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c := h₂ ▸ h₁

Mathlib/Logic/Basic.lean

@@ -527,23 +527,17 @@ theorem ball_mem_comm {α β} [Membership α β] {s : β} {p : α → α → Pro
   ball_cond_comm
 #align ball_mem_comm ball_mem_comm
 
-theorem ne_of_apply_ne {α β : Sort*} (f : α → β) {x y : α} (h : f x ≠ f y) : x ≠ y :=
-  fun w : x = y ↦ h (congr_arg f w)
 #align ne_of_apply_ne ne_of_apply_ne
 
 theorem eq_equivalence : Equivalence (@Eq α) :=
   ⟨Eq.refl, @Eq.symm _, @Eq.trans _⟩
 #align eq_equivalence eq_equivalence
 
-@[simp] theorem eq_mp_eq_cast (h : α = β) : Eq.mp h = cast h := rfl
-#align eq_mp_eq_cast eq_mp_eq_cast
+-- These were migrated to Std but the `@[simp]` attributes were (mysteriously?) removed.
+attribute [simp] eq_mp_eq_cast eq_mpr_eq_cast
 
-@[simp] theorem eq_mpr_eq_cast (h : α = β) : Eq.mpr h = cast h.symm := rfl
+#align eq_mp_eq_cast eq_mp_eq_cast
 #align eq_mpr_eq_cast eq_mpr_eq_cast
-
-@[simp] theorem cast_cast : ∀ (ha : α = β) (hb : β = γ) (a : α),
-    cast hb (cast ha a) = cast (ha.trans hb) a
-  | rfl, rfl, _ => rfl
 #align cast_cast cast_cast
 
 -- @[simp] -- FIXME simp ignores proof rewrites
@@ -569,12 +563,7 @@ theorem congr_fun_congr_arg (f : α → β → γ) {a a' : α} (p : a = a') (b :
     congr_fun (congr_arg f p) b = congr_arg (fun a ↦ f a b) p := rfl
 #align congr_fun_congr_arg congr_fun_congr_arg
 
-theorem heq_of_cast_eq : ∀ (e : α = β) (_ : cast e a = a'), HEq a a'
-  | rfl, h => Eq.recOn h (HEq.refl _)
 #align heq_of_cast_eq heq_of_cast_eq
-
-theorem cast_eq_iff_heq : cast e a = a' ↔ HEq a a' :=
-  ⟨heq_of_cast_eq _, fun h ↦ by cases h; rfl⟩
 #align cast_eq_iff_heq cast_eq_iff_heq
 
 theorem Eq.rec_eq_cast {α : Sort _} {P : α → Sort _} {x y : α} (h : x = y) (z : P x) :
@@ -598,36 +587,16 @@ theorem heq_rec_iff_heq {C : α → Sort*} {x : β} {y : C a} {e : a = b} :
     HEq x (e ▸ y) ↔ HEq x y := by subst e; rfl
 #align heq_rec_iff_heq heq_rec_iff_heq
 
-protected theorem Eq.congr (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) : x₁ = x₂ ↔ y₁ = y₂ := by
-  subst h₁; subst h₂; rfl
 #align eq.congr Eq.congr
-
-theorem Eq.congr_left {x y z : α} (h : x = y) : x = z ↔ y = z := by rw [h]
 #align eq.congr_left Eq.congr_left
-
-theorem Eq.congr_right {x y z : α} (h : x = y) : z = x ↔ z = y := by rw [h]
 #align eq.congr_right Eq.congr_right
-
-alias congr_arg₂ := congrArg₂
 #align congr_arg2 congr_arg₂
 
 variable {β : α → Sort*} {γ : ∀ a, β a → Sort*} {δ : ∀ a b, γ a b → Sort*}
 
-theorem congr_fun₂ {f g : ∀ a b, γ a b} (h : f = g) (a : α) (b : β a) : f a b = g a b :=
-  congr_fun (congr_fun h _) _
 #align congr_fun₂ congr_fun₂
-
-theorem congr_fun₃ {f g : ∀ a b c, δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :
-    f a b c = g a b c :=
-  congr_fun₂ (congr_fun h _) _ _
 #align congr_fun₃ congr_fun₃
-
-theorem funext₂ {f g : ∀ a b, γ a b} (h : ∀ a b, f a b = g a b) : f = g :=
-  funext fun _ ↦ funext <| h _
 #align funext₂ funext₂
-
-theorem funext₃ {f g : ∀ a b c, δ a b c} (h : ∀ a b c, f a b c = g a b c) : f = g :=
-  funext fun _ ↦ funext₂ <| h _
 #align funext₃ funext₃
 
 end Equality

Mathlib/NumberTheory/Divisors.lean

@@ -126,7 +126,8 @@ theorem mem_divisorsAntidiagonal {x : ℕ × ℕ} :
     simp only [succ_le_of_lt (Nat.pos_of_ne_zero h.1), succ_le_of_lt (Nat.pos_of_ne_zero h.2),
       true_and_iff]
     exact
-      ⟨le_mul_of_pos_right (Nat.pos_of_ne_zero h.2), le_mul_of_pos_left (Nat.pos_of_ne_zero h.1)⟩
+      ⟨Nat.le_mul_of_pos_right _ (Nat.pos_of_ne_zero h.2),
+        Nat.le_mul_of_pos_left _ (Nat.pos_of_ne_zero h.1)⟩
 #align nat.mem_divisors_antidiagonal Nat.mem_divisorsAntidiagonal
 
 -- Porting note: Redundant binder annotation update

Mathlib/NumberTheory/FermatPsp.lean

@@ -318,7 +318,7 @@ private theorem psp_from_prime_gt_p {b : ℕ} (b_ge_two : 2 ≤ b) {p : ℕ} (p_
   suffices h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
   · apply gt_of_ge_of_gt
     · exact tsub_le_tsub_left (one_le_of_lt p_gt_two) ((b ^ 2) ^ (p - 1) * b ^ 2)
-    · have : p ≤ p * b ^ 2 := Nat.le_mul_of_pos_right (show 0 < b ^ 2 by nlinarith)
+    · have : p ≤ p * b ^ 2 := Nat.le_mul_of_pos_right _ (show 0 < b ^ 2 by nlinarith)
       exact tsub_lt_tsub_right_of_le this h
   suffices h : p < (b ^ 2) ^ (p - 1)
   · have : 4 ≤ b ^ 2 := by nlinarith
@@ -352,7 +352,7 @@ theorem exists_infinite_pseudoprimes {b : ℕ} (h : 1 ≤ b) (m : ℕ) :
     have h₄ : 0 < b * (b ^ 2 - 1) := mul_pos h₁ h₃
     have h₅ : b * (b ^ 2 - 1) < p := by linarith
     have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅
-    have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right h₃
+    have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right _ h₃
     have h₈ : 2 ≤ b * (b ^ 2 - 1) := le_trans b_ge_two h₇
     have h₉ : 2 < p := gt_of_gt_of_ge h₅ h₈
     have h₁₀ := psp_from_prime_gt_p b_ge_two hp₂ h₉

Mathlib/Tactic/NormNum/LegendreSymbol.lean

@@ -78,8 +78,7 @@ theorem jacobiSymNat.zero_left (b : ℕ) (hb : Nat.beq (b / 2) 0 = false) : jaco
   · calc
       1 < 2 * 1       := by decide
       _ ≤ 2 * (b / 2) :=
-        Nat.mul_le_mul_of_nonneg_left
-          (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb)))
+        Nat.mul_le_mul_left _ (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb)))
       _ ≤ b           := Nat.mul_div_le b 2
 #align norm_num.jacobi_sym_nat.zero_left_even Mathlib.Meta.NormNum.jacobiSymNat.zero_left
 #align norm_num.jacobi_sym_nat.zero_left_odd Mathlib.Meta.NormNum.jacobiSymNat.zero_left

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "c1a3cdf748424810985b479d2712998921c7c797",
+   "rev": "0b2e962a80b98df1c6455f8ae11f2bd16809067c",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "rev": "2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",