From 1e9f59dd323a9da4f45d059916c4f9d5847b6509 Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Wed, 29 Mar 2023 06:53:18 +0000 Subject: [PATCH] chore: forward port leanprover-community/mathlib#18667 (#3163) Co-authored-by: Parcly Taxel --- .../Algebra/Order/Monoid/Canonical/Defs.lean | 14 +++- Mathlib/Algebra/Order/Monoid/MinMax.lean | 71 +++++++++++++------ Mathlib/Order/Basic.lean | 8 ++- 3 files changed, 71 insertions(+), 22 deletions(-) diff --git a/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean b/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean index b45e89608da61..89824a74cd5fb 100644 --- a/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean +++ b/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl ! This file was ported from Lean 3 source module algebra.order.monoid.canonical.defs -! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025 +! leanprover-community/mathlib commit de87d5053a9fe5cbde723172c0fb7e27e7436473 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -189,6 +189,18 @@ theorem le_of_mul_le_right : a * b ≤ c → b ≤ c := #align le_of_mul_le_right le_of_mul_le_right #align le_of_add_le_right le_of_add_le_right +@[to_additive] +theorem le_mul_of_le_left : a ≤ b → a ≤ b * c := + le_self_mul.trans' +#align le_mul_of_le_left le_mul_of_le_left +#align le_add_of_le_left le_add_of_le_left + +@[to_additive] +theorem le_mul_of_le_right : a ≤ c → a ≤ b * c := + le_mul_self.trans' +#align le_mul_of_le_right le_mul_of_le_right +#align le_add_of_le_right le_add_of_le_right + @[to_additive] theorem le_iff_exists_mul : a ≤ b ↔ ∃ c, b = a * c := ⟨exists_mul_of_le, by diff --git a/Mathlib/Algebra/Order/Monoid/MinMax.lean b/Mathlib/Algebra/Order/Monoid/MinMax.lean index ccfd9595d3f1c..0056bdee297b0 100644 --- a/Mathlib/Algebra/Order/Monoid/MinMax.lean +++ b/Mathlib/Algebra/Order/Monoid/MinMax.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl ! This file was ported from Lean 3 source module algebra.order.monoid.min_max -! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025 +! leanprover-community/mathlib commit de87d5053a9fe5cbde723172c0fb7e27e7436473 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -17,6 +17,8 @@ import Mathlib.Tactic.Contrapose -/ +open Function + variable {α β : Type _} /-! Some lemmas about types that have an ordering and a binary operation, with no @@ -59,25 +61,6 @@ theorem max_mul_mul_left (a b c : α) : max (a * b) (a * c) = a * max b c := #align max_mul_mul_left max_mul_mul_left #align max_add_add_left max_add_add_left -@[to_additive] -theorem lt_or_lt_of_mul_lt_mul [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a b m n : α} - (h : m * n < a * b) : m < a ∨ n < b := by - contrapose! h - exact mul_le_mul' h.1 h.2 -#align lt_or_lt_of_mul_lt_mul lt_or_lt_of_mul_lt_mul -#align lt_or_lt_of_add_lt_add lt_or_lt_of_add_lt_add - -@[to_additive] -theorem mul_lt_mul_iff_of_le_of_le [CovariantClass α α (Function.swap (· * ·)) (· < ·)] - [CovariantClass α α (· * ·) (· < ·)] [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] - {a b c d : α} (ac : a ≤ c) (bd : b ≤ d) : a * b < c * d ↔ a < c ∨ b < d := by - refine' ⟨lt_or_lt_of_mul_lt_mul, fun h => _⟩ - cases' h with ha hb - · exact mul_lt_mul_of_lt_of_le ha bd - · exact mul_lt_mul_of_le_of_lt ac hb -#align mul_lt_mul_iff_of_le_of_le mul_lt_mul_iff_of_le_of_le -#align add_lt_add_iff_of_le_of_le add_lt_add_iff_of_le_of_le - end Left section Right @@ -98,6 +81,54 @@ theorem max_mul_mul_right (a b c : α) : max (a * c) (b * c) = max a b * c := end Right +@[to_additive] +theorem lt_or_lt_of_mul_lt_mul [CovariantClass α α (· * ·) (· ≤ ·)] + [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a₁ a₂ b₁ b₂ : α} : + a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂ := by + contrapose! + exact fun h => mul_le_mul' h.1 h.2 +#align lt_or_lt_of_mul_lt_mul lt_or_lt_of_mul_lt_mul +#align lt_or_lt_of_add_lt_add lt_or_lt_of_add_lt_add + +@[to_additive] +theorem le_or_lt_of_mul_le_mul [CovariantClass α α (· * ·) (· ≤ ·)] + [CovariantClass α α (Function.swap (· * ·)) (· < ·)] {a₁ a₂ b₁ b₂ : α} : + a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂ := by + contrapose! + exact fun h => mul_lt_mul_of_lt_of_le h.1 h.2 +#align le_or_lt_of_mul_le_mul le_or_lt_of_mul_le_mul +#align le_or_lt_of_add_le_add le_or_lt_of_add_le_add + +@[to_additive] +theorem lt_or_le_of_mul_le_mul [CovariantClass α α (· * ·) (· < ·)] + [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a₁ a₂ b₁ b₂ : α} : + a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂ := by + contrapose! + exact fun h => mul_lt_mul_of_le_of_lt h.1 h.2 +#align lt_or_le_of_mul_le_mul lt_or_le_of_mul_le_mul +#align lt_or_le_of_add_le_add lt_or_le_of_add_le_add + +@[to_additive] +theorem le_or_le_of_mul_le_mul [CovariantClass α α (· * ·) (· < ·)] + [CovariantClass α α (Function.swap (· * ·)) (· < ·)] {a₁ a₂ b₁ b₂ : α} : + a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂ := by + contrapose! + exact fun h => mul_lt_mul_of_lt_of_lt h.1 h.2 +#align le_or_le_of_mul_le_mul le_or_le_of_mul_le_mul +#align le_or_le_of_add_le_add le_or_le_of_add_le_add + +@[to_additive] +theorem mul_lt_mul_iff_of_le_of_le [CovariantClass α α (· * ·) (· ≤ ·)] + [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] [CovariantClass α α (· * ·) (· < ·)] + [CovariantClass α α (Function.swap (· * ·)) (· < ·)] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) + (hb : b₁ ≤ b₂) : a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂ := by + refine' ⟨lt_or_lt_of_mul_lt_mul, fun h => _⟩ + cases' h with ha' hb' + · exact mul_lt_mul_of_lt_of_le ha' hb + · exact mul_lt_mul_of_le_of_lt ha hb' +#align mul_lt_mul_iff_of_le_of_le mul_lt_mul_iff_of_le_of_le +#align add_lt_add_iff_of_le_of_le add_lt_add_iff_of_le_of_le + end Mul variable [MulOneClass α] diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean index 564c260a4c2e1..d99fb830001c2 100644 --- a/Mathlib/Order/Basic.lean +++ b/Mathlib/Order/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Mario Carneiro ! This file was ported from Lean 3 source module order.basic -! leanprover-community/mathlib commit 1f0096e6caa61e9c849ec2adbd227e960e9dff58 +! leanprover-community/mathlib commit de87d5053a9fe5cbde723172c0fb7e27e7436473 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -404,12 +404,18 @@ theorem eq_or_gt_of_le [PartialOrder α] {a b : α} (h : a ≤ b) : b = a ∨ a h.lt_or_eq.symm.imp Eq.symm id #align eq_or_gt_of_le eq_or_gt_of_le +theorem gt_or_eq_of_le [PartialOrder α] {a b : α} (h : a ≤ b) : a < b ∨ b = a := + (eq_or_gt_of_le h).symm +#align gt_or_eq_of_le gt_or_eq_of_le + alias Decidable.eq_or_lt_of_le ← LE.le.eq_or_lt_dec alias eq_or_lt_of_le ← LE.le.eq_or_lt alias eq_or_gt_of_le ← LE.le.eq_or_gt +alias gt_or_eq_of_le ← LE.le.gt_or_eq + -- Porting note: no `decidable_classical` linter -- attribute [nolint decidable_classical] LE.le.eq_or_lt_dec