chore: forward port leanprover-community/mathlib#18667 (#3163)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

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

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 α]

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