From 59d9e5bffd8de2b74c95f2cff2389832f1e07c79 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Mon, 24 Jul 2023 11:23:08 -0400 Subject: [PATCH] fix: patch for std4#198 --- .../Algebra/EuclideanDomain/Instances.lean | 2 +- .../SimpleGraph/Regularity/Bound.lean | 5 +++-- .../SimpleGraph/Regularity/Equitabilise.lean | 9 ++++---- Mathlib/Data/FP/Basic.lean | 2 +- Mathlib/Data/List/Rotate.lean | 2 +- Mathlib/Data/Nat/Basic.lean | 4 ++-- Mathlib/Data/Nat/Choose/Central.lean | 6 ++--- Mathlib/Data/Nat/Factorial/Basic.lean | 22 +++++++++---------- .../Data/Nat/Factorial/DoubleFactorial.lean | 2 +- Mathlib/Data/Nat/Fib/Basic.lean | 2 +- Mathlib/Data/Nat/Order/Basic.lean | 14 +++--------- Mathlib/Data/Nat/Sqrt.lean | 2 +- Mathlib/Data/ZMod/Basic.lean | 2 +- Mathlib/FieldTheory/SeparableDegree.lean | 4 ++-- Mathlib/Init/Data/Nat/Lemmas.lean | 2 +- Mathlib/NumberTheory/Divisors.lean | 3 ++- Mathlib/NumberTheory/FermatPsp.lean | 4 ++-- Mathlib/Tactic/NormNum/LegendreSymbol.lean | 3 +-- lake-manifest.json | 4 ++-- test/apply_rules.lean | 6 ++--- 20 files changed, 47 insertions(+), 53 deletions(-) diff --git a/Mathlib/Algebra/EuclideanDomain/Instances.lean b/Mathlib/Algebra/EuclideanDomain/Instances.lean index 87c43b6a42342..a9ae72c47a1a4 100644 --- a/Mathlib/Algebra/EuclideanDomain/Instances.lean +++ b/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 := diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean index 913cb8c960844..0650031e79e9a 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean +++ b/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 => @@ -215,7 +216,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 := diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean index 92fd8bf443629..402d1657d693c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean +++ b/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 diff --git a/Mathlib/Data/FP/Basic.lean b/Mathlib/Data/FP/Basic.lean index d1d2bb060cc8a..b25939dd146ce 100644 --- a/Mathlib/Data/FP/Basic.lean +++ b/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 diff --git a/Mathlib/Data/List/Rotate.lean b/Mathlib/Data/List/Rotate.lean index 57eb4489f6762..c20b92ff365b3 100644 --- a/Mathlib/Data/List/Rotate.lean +++ b/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 := diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean index d1e8dea049591..257e9356c94df 100644 --- a/Mathlib/Data/Nat/Basic.lean +++ b/Mathlib/Data/Nat/Basic.lean @@ -380,8 +380,8 @@ lemma one_lt_mul_iff : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n) := by · simp at h · exact (Nat.mul_le_mul h'.1 h'.2).not_lt 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 h.2.1 + · exact Nat.mul_lt_mul_of_le_of_lt h.1 hn h.1 /-! ### Recursion and induction principles diff --git a/Mathlib/Data/Nat/Choose/Central.lean b/Mathlib/Data/Nat/Choose/Central.lean index 95b68c78116e8..c7e350182294c 100644 --- a/Mathlib/Data/Nat/Choose/Central.lean +++ b/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 diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean index 14afd1fc03435..e21fae4d62653 100644 --- a/Mathlib/Data/Nat/Factorial/Basic.lean +++ b/Mathlib/Data/Nat/Factorial/Basic.lean @@ -274,11 +274,15 @@ theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, (n + 1) ^ k ≤ n.ascF exact Nat.mul_le_mul (Nat.add_le_add_right le_self_add _) (pow_succ_le_ascFactorial _ k) #align nat.pow_succ_le_asc_factorial Nat.pow_succ_le_ascFactorial +theorem ascFactorial_pos (n k : ℕ) : 0 < n.ascFactorial k := + (pow_pos (succ_pos n) k).trans_le (pow_succ_le_ascFactorial n k) +#align nat.asc_factorial_pos Nat.ascFactorial_pos + theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < n.ascFactorial (k + 2) := by rw [pow_succ, ascFactorial, mul_comm] exact - Nat.mul_lt_mul (Nat.add_lt_add_right (Nat.lt_add_of_pos_right succ_pos') 1) - (pow_succ_le_ascFactorial n _) (pow_pos succ_pos' _) + Nat.mul_lt_mul_of_lt_of_le (Nat.add_lt_add_right (Nat.lt_add_of_pos_right succ_pos') 1) + (pow_succ_le_ascFactorial n _) (ascFactorial_pos _ _) #align nat.pow_lt_asc_factorial' Nat.pow_lt_ascFactorial' theorem pow_lt_ascFactorial (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1) ^ k < n.ascFactorial k @@ -292,8 +296,8 @@ theorem ascFactorial_le_pow_add (n : ℕ) : ∀ k : ℕ, n.ascFactorial k ≤ (n | k + 1 => by rw [ascFactorial_succ, pow_succ, ← add_assoc, mul_comm _ (succ (n + k))] exact - Nat.mul_le_mul_of_nonneg_left - ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_left (le_succ _) _)) + Nat.mul_le_mul_left _ + ((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 theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → n.ascFactorial k < (n + k) ^ k @@ -306,10 +310,6 @@ theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → n.ascFact Nat.pow_lt_pow_left (lt_add_one _) k.succ_ne_zero) (succ_pos _) #align nat.asc_factorial_lt_pow_add Nat.ascFactorial_lt_pow_add -theorem ascFactorial_pos (n k : ℕ) : 0 < n.ascFactorial k := - (pow_pos (succ_pos n) k).trans_le (pow_succ_le_ascFactorial n k) -#align nat.asc_factorial_pos Nat.ascFactorial_pos - end AscFactorial section DescFactorial @@ -401,8 +401,8 @@ 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 - exact (le_trans (Nat.pow_le_pow_left (tsub_le_tsub_right (le_succ _) _) k) + apply Nat.mul_le_mul_left + exact (le_trans (Nat.pow_le_pow_of_le_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 @@ -443,7 +443,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 diff --git a/Mathlib/Data/Nat/Factorial/DoubleFactorial.lean b/Mathlib/Data/Nat/Factorial/DoubleFactorial.lean index 1bda3a8a658b5..2b9bd1eb1b5a3 100644 --- a/Mathlib/Data/Nat/Factorial/DoubleFactorial.lean +++ b/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 diff --git a/Mathlib/Data/Nat/Fib/Basic.lean b/Mathlib/Data/Nat/Fib/Basic.lean index 905e749542abf..c8df30541f31b 100644 --- a/Mathlib/Data/Nat/Fib/Basic.lean +++ b/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 diff --git a/Mathlib/Data/Nat/Order/Basic.lean b/Mathlib/Data/Nat/Order/Basic.lean index 3d62c7d35d091..91aca16e6efdc 100644 --- a/Mathlib/Data/Nat/Order/Basic.lean +++ b/Mathlib/Data/Nat/Order/Basic.lean @@ -288,18 +288,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 := @@ -476,7 +468,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`. -/ diff --git a/Mathlib/Data/Nat/Sqrt.lean b/Mathlib/Data/Nat/Sqrt.lean index a56d4127ff713..4e5a2e25f50a5 100644 --- a/Mathlib/Data/Nat/Sqrt.lean +++ b/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 _ diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean index 0f5fa03ee8070..2e65ebc2dfdb9 100644 --- a/Mathlib/Data/ZMod/Basic.lean +++ b/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 diff --git a/Mathlib/FieldTheory/SeparableDegree.lean b/Mathlib/FieldTheory/SeparableDegree.lean index ff9f8f743c017..cd2c56c726ba7 100644 --- a/Mathlib/FieldTheory/SeparableDegree.lean +++ b/Mathlib/FieldTheory/SeparableDegree.lean @@ -583,7 +583,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 ↦ ?_) ⊤ @@ -603,7 +603,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⟩ diff --git a/Mathlib/Init/Data/Nat/Lemmas.lean b/Mathlib/Init/Data/Nat/Lemmas.lean index 25a14c70fd10b..aab00da66c79d 100644 --- a/Mathlib/Init/Data/Nat/Lemmas.lean +++ b/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 -/ diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean index cff3ebc327baa..ba79462e0470c 100644 --- a/Mathlib/NumberTheory/Divisors.lean +++ b/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 diff --git a/Mathlib/NumberTheory/FermatPsp.lean b/Mathlib/NumberTheory/FermatPsp.lean index 7a2db88a60b5d..244df563715a3 100644 --- a/Mathlib/NumberTheory/FermatPsp.lean +++ b/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₉ diff --git a/Mathlib/Tactic/NormNum/LegendreSymbol.lean b/Mathlib/Tactic/NormNum/LegendreSymbol.lean index 8417a02e44a34..730f2de9e9aba 100644 --- a/Mathlib/Tactic/NormNum/LegendreSymbol.lean +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index a3715f895d767..0402f1719bce5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "0f6bc5b32bf5b0498902d3b5f0806c75530539d5", + "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", diff --git a/test/apply_rules.lean b/test/apply_rules.lean index aa04f6d0f8d46..9cb435a6580ce 100644 --- a/test/apply_rules.lean +++ b/test/apply_rules.lean @@ -7,17 +7,17 @@ open Nat example {a b c d e : Nat} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) : a + c * e + a + c + 0 ≤ b + d * e + b + d + e := Nat.add_le_add (Nat.add_le_add (Nat.add_le_add - (Nat.add_le_add h1 (Nat.mul_le_mul_of_nonneg_right h2)) h1) h2) h3 + (Nat.add_le_add h1 (Nat.mul_le_mul_right _ h2)) h1) h2) h3 example {a b c d e : Nat} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) : a + c * e + a + c + 0 ≤ b + d * e + b + d + e := by - apply_rules [Nat.add_le_add, Nat.mul_le_mul_of_nonneg_right] + apply_rules [Nat.add_le_add, Nat.mul_le_mul_right] -- Check that when we supply an iteration bound, -- `apply_rules` works up to that bound and returns the remaining goals. example {a b c d e : Nat} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) : a + c * e + a + c + 0 ≤ b + d * e + b + d + e := by - apply_rules (config := {maxDepth := 9}) [Nat.add_le_add, Nat.mul_le_mul_of_nonneg_right] + apply_rules (config := {maxDepth := 9}) [Nat.add_le_add, Nat.mul_le_mul_right] guard_target = 0 ≤ e assumption