chore: forward-port leanprover-community/mathlib3#18831 (#3572)

Mathlib/Algebra/Order/Field/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 ! This file was ported from Lean 3 source module algebra.order.field.basic
-! leanprover-community/mathlib commit acb3d204d4ee883eb686f45d486a2a6811a01329
+! leanprover-community/mathlib commit 44e29dbcff83ba7114a464d592b8c3743987c1e5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -742,6 +742,10 @@ theorem lt_div_iff_of_neg' (hc : c < 0) : a < b / c ↔ b < c * a := by
   rw [mul_comm, lt_div_iff_of_neg hc]
 #align lt_div_iff_of_neg' lt_div_iff_of_neg'
 
+theorem div_le_one_of_ge (h : b ≤ a) (hb : b ≤ 0) : a / b ≤ 1 := by
+  simpa only [neg_div_neg_eq] using div_le_one_of_le (neg_le_neg h) (neg_nonneg_of_nonpos hb)
+#align div_le_one_of_ge div_le_one_of_ge
+
 /-! ### Bi-implications of inequalities using inversions -/
 
 

Mathlib/Algebra/Order/Ring/Defs.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Yaël Dillies
 Ported by: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.order.ring.defs
-! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94
+! leanprover-community/mathlib commit 44e29dbcff83ba7114a464d592b8c3743987c1e5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -392,6 +392,26 @@ theorem mul_le_mul_of_nonpos_of_nonpos' (hca : c ≤ a) (hdb : d ≤ b) (ha : a
   (mul_le_mul_of_nonpos_left hdb ha).trans <| mul_le_mul_of_nonpos_right hca hd
 #align mul_le_mul_of_nonpos_of_nonpos' mul_le_mul_of_nonpos_of_nonpos'
 
+/-- Variant of `mul_le_of_le_one_left` for `b` non-positive instead of non-negative.  -/
+theorem le_mul_of_le_one_left (hb : b ≤ 0) (h : a ≤ 1) : b ≤ a * b := by
+  simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb
+#align le_mul_of_le_one_left le_mul_of_le_one_left
+
+/-- Variant of `le_mul_of_one_le_left` for `b` non-positive instead of non-negative. -/
+theorem mul_le_of_one_le_left (hb : b ≤ 0) (h : 1 ≤ a) : a * b ≤ b := by
+  simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb
+#align mul_le_of_one_le_left mul_le_of_one_le_left
+
+/-- Variant of `mul_le_of_le_one_right` for `a` non-positive instead of non-negative. -/
+theorem le_mul_of_le_one_right (ha : a ≤ 0) (h : b ≤ 1) : a ≤ a * b := by
+  simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha
+#align le_mul_of_le_one_right le_mul_of_le_one_right
+
+/-- Variant of `le_mul_of_one_le_right` for `a` non-positive instead of non-negative. -/
+theorem mul_le_of_one_le_right (ha : a ≤ 0) (h : 1 ≤ b) : a * b ≤ a := by
+  simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha
+#align mul_le_of_one_le_right mul_le_of_one_le_right
+
 section Monotone
 
 variable [Preorder β] {f g : β → α}
@@ -681,6 +701,26 @@ theorem mul_pos_of_neg_of_neg {a b : α} (ha : a < 0) (hb : b < 0) : 0 < a * b :
   simpa only [zero_mul] using mul_lt_mul_of_neg_right ha hb
 #align mul_pos_of_neg_of_neg mul_pos_of_neg_of_neg
 
+/-- Variant of `mul_lt_of_lt_one_left` for `b` negative instead of positive. -/
+theorem lt_mul_of_lt_one_left (hb : b < 0) (h : a < 1) : b < a * b := by
+  simpa only [one_mul] using mul_lt_mul_of_neg_right h hb
+#align lt_mul_of_lt_one_left lt_mul_of_lt_one_left
+
+/-- Variant of `lt_mul_of_one_lt_left` for `b` negative instead of positive. -/
+theorem mul_lt_of_one_lt_left (hb : b < 0) (h : 1 < a) : a * b < b := by
+  simpa only [one_mul] using mul_lt_mul_of_neg_right h hb
+#align mul_lt_of_one_lt_left mul_lt_of_one_lt_left
+
+/-- Variant of `mul_lt_of_lt_one_right` for `a` negative instead of positive. -/
+theorem lt_mul_of_lt_one_right (ha : a < 0) (h : b < 1) : a < a * b := by
+  simpa only [mul_one] using mul_lt_mul_of_neg_left h ha
+#align lt_mul_of_lt_one_right lt_mul_of_lt_one_right
+
+/-- Variant of `lt_mul_of_lt_one_right` for `a` negative instead of positive. -/
+theorem mul_lt_of_one_lt_right (ha : a < 0) (h : 1 < b) : a * b < a := by
+  simpa only [mul_one] using mul_lt_mul_of_neg_left h ha
+#align mul_lt_of_one_lt_right mul_lt_of_one_lt_right
+
 section Monotone
 
 variable [Preorder β] {f g : β → α}

Mathlib/Algebra/Order/Ring/Lemmas.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Yuyang Zhao
 
 ! This file was ported from Lean 3 source module algebra.order.ring.lemmas
-! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
+! leanprover-community/mathlib commit 44e29dbcff83ba7114a464d592b8c3743987c1e5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -660,7 +660,10 @@ theorem mul_lt_iff_lt_one_left [MulPosStrictMono α] [MulPosReflectLT α] (b0 :
   Iff.trans (by rw [one_mul]) (mul_lt_mul_right b0)
 #align mul_lt_iff_lt_one_left mul_lt_iff_lt_one_left
 
-/-! Lemmas of the form `1 ≤ b → a ≤ a * b`. -/
+/-! Lemmas of the form `1 ≤ b → a ≤ a * b`.
+
+Variants with `< 0` and `≤ 0` instead of `0 <` and `0 ≤` appear in `Mathlib/Algebra/Order/Ring/Defs`
+(which imports this file) as they need additional results which are not yet available here. -/
 
 
 theorem mul_le_of_le_one_left [MulPosMono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b := by