chore (Algebra.Order.Field.Defs): split off results about unbundled ordered algebra (#14451)

We should be able to use these results about unbundled ordered algebra without importing the heavy machinery of the bundled typeclasses.

Author: mattrobball

Mathlib.lean

@@ -531,6 +531,7 @@ import Mathlib.Algebra.Order.Field.Pi
 import Mathlib.Algebra.Order.Field.Power
 import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Algebra.Order.Field.Subfield
+import Mathlib.Algebra.Order.Field.Unbundled.Basic
 import Mathlib.Algebra.Order.Floor
 import Mathlib.Algebra.Order.Floor.Div
 import Mathlib.Algebra.Order.Floor.Prime

Mathlib/Algebra/Order/Field/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Order.Bounds.OrderIso
 import Mathlib.Tactic.Positivity.Core
+import Mathlib.Algebra.Order.Field.Unbundled.Basic
 
 #align_import algebra.order.field.basic from "leanprover-community/mathlib"@"84771a9f5f0bd5e5d6218811556508ddf476dcbd"
 
@@ -49,7 +50,7 @@ theorem le_div_iff (hc : 0 < c) : a ≤ b / c ↔ a * c ≤ b :=
   ⟨fun h => div_mul_cancel₀ b (ne_of_lt hc).symm ▸ mul_le_mul_of_nonneg_right h hc.le, fun h =>
     calc
       a = a * c * (1 / c) := mul_mul_div a (ne_of_lt hc).symm
-      _ ≤ b * (1 / c) := mul_le_mul_of_nonneg_right h (one_div_pos.2 hc).le
+      _ ≤ b * (1 / c) := mul_le_mul_of_nonneg_right h (one_div_pos (α := α) |>.2 hc).le
       _ = b / c := (div_eq_mul_one_div b c).symm
       ⟩
 #align le_div_iff le_div_iff
@@ -66,7 +67,7 @@ theorem div_le_iff (hb : 0 < b) : a / b ≤ c ↔ a ≤ c * b :=
     fun h =>
     calc
       a / b = a * (1 / b) := div_eq_mul_one_div a b
-      _ ≤ c * b * (1 / b) := mul_le_mul_of_nonneg_right h (one_div_pos.2 hb).le
+      _ ≤ c * b * (1 / b) := mul_le_mul_of_nonneg_right h (one_div_pos (α := α) |>.2 hb).le
       _ = c * b / b := (div_eq_mul_one_div (c * b) b).symm
       _ = c := by refine (div_eq_iff (ne_of_gt hb)).mpr rfl
       ⟩
@@ -188,15 +189,15 @@ theorem inv_le_inv (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
 /-- In a linear ordered field, for positive `a` and `b` we have `a⁻¹ ≤ b ↔ b⁻¹ ≤ a`.
 See also `inv_le_of_inv_le` for a one-sided implication with one fewer assumption. -/
 theorem inv_le (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a := by
-  rw [← inv_le_inv hb (inv_pos.2 ha), inv_inv]
+  rw [← inv_le_inv hb (inv_pos (α := α) |>.2 ha), inv_inv]
 #align inv_le inv_le
 
 theorem inv_le_of_inv_le (ha : 0 < a) (h : a⁻¹ ≤ b) : b⁻¹ ≤ a :=
-  (inv_le ha ((inv_pos.2 ha).trans_le h)).1 h
+  (inv_le ha ((inv_pos (α := α) |>.2 ha).trans_le h)).1 h
 #align inv_le_of_inv_le inv_le_of_inv_le
 
 theorem le_inv (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹ := by
-  rw [← inv_le_inv (inv_pos.2 hb) ha, inv_inv]
+  rw [← inv_le_inv (inv_pos (α := α) |>.2 hb) ha, inv_inv]
 #align le_inv le_inv
 
 /-- See `inv_lt_inv_of_lt` for the implication from right-to-left with one fewer assumption. -/
@@ -216,7 +217,7 @@ theorem inv_lt (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b ↔ b⁻¹ < a :=
 #align inv_lt inv_lt
 
 theorem inv_lt_of_inv_lt (ha : 0 < a) (h : a⁻¹ < b) : b⁻¹ < a :=
-  (inv_lt ha ((inv_pos.2 ha).trans h)).1 h
+  (inv_lt ha ((inv_pos (α := α) |>.2 ha).trans h)).1 h
 #align inv_lt_of_inv_lt inv_lt_of_inv_lt
 
 theorem lt_inv (ha : 0 < a) (hb : 0 < b) : a < b⁻¹ ↔ b < a⁻¹ :=
@@ -240,17 +241,18 @@ theorem one_le_inv (h₁ : 0 < a) (h₂ : a ≤ 1) : 1 ≤ a⁻¹ := by
 #align one_le_inv one_le_inv
 
 theorem inv_lt_one_iff_of_pos (h₀ : 0 < a) : a⁻¹ < 1 ↔ 1 < a :=
-  ⟨fun h₁ => inv_inv a ▸ one_lt_inv (inv_pos.2 h₀) h₁, inv_lt_one⟩
+  ⟨fun h₁ => inv_inv a ▸ one_lt_inv (inv_pos (α := α) |>.2 h₀) h₁, inv_lt_one⟩
 #align inv_lt_one_iff_of_pos inv_lt_one_iff_of_pos
 
 theorem inv_lt_one_iff : a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a := by
   rcases le_or_lt a 0 with ha | ha
-  · simp [ha, (inv_nonpos.2 ha).trans_lt zero_lt_one]
+  · simp [ha, (inv_nonpos (α := α) |>.2 ha).trans_lt zero_lt_one]
   · simp only [ha.not_le, false_or_iff, inv_lt_one_iff_of_pos ha]
 #align inv_lt_one_iff inv_lt_one_iff
 
 theorem one_lt_inv_iff : 1 < a⁻¹ ↔ 0 < a ∧ a < 1 :=
-  ⟨fun h => ⟨inv_pos.1 (zero_lt_one.trans h), inv_inv a ▸ inv_lt_one h⟩, and_imp.2 one_lt_inv⟩
+  ⟨fun h => ⟨inv_pos (α := α) |>.1 (zero_lt_one.trans h),
+    inv_inv a ▸ inv_lt_one h⟩, and_imp.2 one_lt_inv⟩
 #align one_lt_inv_iff one_lt_inv_iff
 
 theorem inv_le_one_iff : a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a := by
@@ -260,7 +262,8 @@ theorem inv_le_one_iff : a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a := by
 #align inv_le_one_iff inv_le_one_iff
 
 theorem one_le_inv_iff : 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1 :=
-  ⟨fun h => ⟨inv_pos.1 (zero_lt_one.trans_le h), inv_inv a ▸ inv_le_one h⟩, and_imp.2 one_le_inv⟩
+  ⟨fun h => ⟨inv_pos (α := α) |>.1 (zero_lt_one.trans_le h),
+    inv_inv a ▸ inv_le_one h⟩, and_imp.2 one_le_inv⟩
 #align one_le_inv_iff one_le_inv_iff
 
 /-!
@@ -271,13 +274,13 @@ theorem one_le_inv_iff : 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1 :=
 @[mono, gcongr]
 lemma div_le_div_of_nonneg_right (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c := by
   rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
-  exact mul_le_mul_of_nonneg_right hab (one_div_nonneg.2 hc)
+  exact mul_le_mul_of_nonneg_right hab (one_div_nonneg (α := α) |>.2 hc)
 #align div_le_div_of_le_of_nonneg div_le_div_of_nonneg_right
 
 @[gcongr]
 lemma div_lt_div_of_pos_right (h : a < b) (hc : 0 < c) : a / c < b / c := by
   rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
-  exact mul_lt_mul_of_pos_right h (one_div_pos.2 hc)
+  exact mul_lt_mul_of_pos_right h (one_div_pos (α := α) |>.2 hc)
 #align div_lt_div_of_lt div_lt_div_of_pos_right
 
 -- Not a `mono` lemma b/c `div_le_div` is strictly more general
@@ -482,7 +485,7 @@ theorem add_thirds (a : α) : a / 3 + a / 3 + a / 3 = a := by
   simp only [div_eq_mul_inv, mul_pos_iff_of_pos_left ha, inv_pos]
 
 @[simp] lemma div_pos_iff_of_pos_right (hb : 0 < b) : 0 < a / b ↔ 0 < a := by
-  simp only [div_eq_mul_inv, mul_pos_iff_of_pos_right (inv_pos.2 hb)]
+  simp only [div_eq_mul_inv, mul_pos_iff_of_pos_right (inv_pos (α := α) |>.2 hb)]
 
 theorem mul_le_mul_of_mul_div_le (h : a * (b / c) ≤ d) (hc : 0 < c) : b * a ≤ d * c := by
   rw [← mul_div_assoc] at h
@@ -492,7 +495,7 @@ theorem mul_le_mul_of_mul_div_le (h : a * (b / c) ≤ d) (hc : 0 < c) : b * a 
 theorem div_mul_le_div_mul_of_div_le_div (h : a / b ≤ c / d) (he : 0 ≤ e) :
     a / (b * e) ≤ c / (d * e) := by
   rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div]
-  exact mul_le_mul_of_nonneg_right h (one_div_nonneg.2 he)
+  exact mul_le_mul_of_nonneg_right h (one_div_nonneg (α := α) |>.2 he)
 #align div_mul_le_div_mul_of_div_le_div div_mul_le_div_mul_of_div_le_div
 
 theorem exists_pos_mul_lt {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b * c < a := by
@@ -504,7 +507,7 @@ theorem exists_pos_mul_lt {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧
 
 theorem exists_pos_lt_mul {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b < c * a :=
   let ⟨c, hc₀, hc⟩ := exists_pos_mul_lt h b;
-  ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff hc₀]⟩
+  ⟨c⁻¹, inv_pos (α := α) |>.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff hc₀]⟩
 #align exists_pos_lt_mul exists_pos_lt_mul
 
 lemma monotone_div_right_of_nonneg (ha : 0 ≤ a) : Monotone (· / a) :=
@@ -519,7 +522,7 @@ theorem Monotone.div_const {β : Type*} [Preorder β] {f : β → α} (hf : Mono
 
 theorem StrictMono.div_const {β : Type*} [Preorder β] {f : β → α} (hf : StrictMono f) {c : α}
     (hc : 0 < c) : StrictMono fun x => f x / c := by
-  simpa only [div_eq_mul_inv] using hf.mul_const (inv_pos.2 hc)
+  simpa only [div_eq_mul_inv] using hf.mul_const (inv_pos (α := α) |>.2 hc)
 #align strict_mono.div_const StrictMono.div_const
 
 -- see Note [lower instance priority]
@@ -652,7 +655,7 @@ theorem div_le_iff_of_neg (hc : c < 0) : b / c ≤ a ↔ a * c ≤ b :=
   ⟨fun h => div_mul_cancel₀ b (ne_of_lt hc) ▸ mul_le_mul_of_nonpos_right h hc.le, fun h =>
     calc
       a = a * c * (1 / c) := mul_mul_div a (ne_of_lt hc)
-      _ ≥ b * (1 / c) := mul_le_mul_of_nonpos_right h (one_div_neg.2 hc).le
+      _ ≥ b * (1 / c) := mul_le_mul_of_nonpos_right h (one_div_neg (α := α) |>.2 hc).le
       _ = b / c := (div_eq_mul_one_div b c).symm
       ⟩
 #align div_le_iff_of_neg div_le_iff_of_neg
@@ -697,11 +700,11 @@ theorem inv_le_inv_of_neg (ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b⁻¹ ↔ b 
 #align inv_le_inv_of_neg inv_le_inv_of_neg
 
 theorem inv_le_of_neg (ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a := by
-  rw [← inv_le_inv_of_neg hb (inv_lt_zero.2 ha), inv_inv]
+  rw [← inv_le_inv_of_neg hb (inv_lt_zero (α := α) |>.2 ha), inv_inv]
 #align inv_le_of_neg inv_le_of_neg
 
 theorem le_inv_of_neg (ha : a < 0) (hb : b < 0) : a ≤ b⁻¹ ↔ b ≤ a⁻¹ := by
-  rw [← inv_le_inv_of_neg (inv_lt_zero.2 hb) ha, inv_inv]
+  rw [← inv_le_inv_of_neg (inv_lt_zero (α := α) |>.2 hb) ha, inv_inv]
 #align le_inv_of_neg le_inv_of_neg
 
 theorem inv_lt_inv_of_neg (ha : a < 0) (hb : b < 0) : a⁻¹ < b⁻¹ ↔ b < a :=
@@ -768,12 +771,12 @@ theorem inv_antitoneOn_Icc_left (hb : b < 0) :
 
 theorem div_le_div_of_nonpos_of_le (hc : c ≤ 0) (h : b ≤ a) : a / c ≤ b / c := by
   rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
-  exact mul_le_mul_of_nonpos_right h (one_div_nonpos.2 hc)
+  exact mul_le_mul_of_nonpos_right h (one_div_nonpos (α := α) |>.2 hc)
 #align div_le_div_of_nonpos_of_le div_le_div_of_nonpos_of_le
 
 theorem div_lt_div_of_neg_of_lt (hc : c < 0) (h : b < a) : a / c < b / c := by
   rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
-  exact mul_lt_mul_of_neg_right h (one_div_neg.2 hc)
+  exact mul_lt_mul_of_neg_right h (one_div_neg (α := α) |>.2 hc)
 #align div_lt_div_of_neg_of_lt div_lt_div_of_neg_of_lt
 
 theorem div_le_div_right_of_neg (hc : c < 0) : a / c ≤ b / c ↔ b ≤ a :=
@@ -905,7 +908,7 @@ theorem add_sub_div_two_lt (h : a < b) : a + (b - a) / 2 < b := by
 /-- An inequality involving `2`. -/
 theorem sub_one_div_inv_le_two (a2 : 2 ≤ a) : (1 - 1 / a)⁻¹ ≤ 2 := by
   -- Take inverses on both sides to obtain `2⁻¹ ≤ 1 - 1 / a`
-  refine (inv_le_inv_of_le (inv_pos.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))
+  refine (inv_le_inv_of_le (inv_pos (α := α) |>.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))
   -- move `1 / a` to the left and `2⁻¹` to the right.
   rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]
   -- take inverses on both sides and use the assumption `2 ≤ a`.

Mathlib/Algebra/Order/Field/Defs.lean

@@ -3,9 +3,8 @@ 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
 -/
-import Mathlib.Algebra.Field.Defs
-import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.Order.Ring.Defs
+import Mathlib.Algebra.Field.Defs
 
 #align_import algebra.order.field.defs from "leanprover-community/mathlib"@"655994e298904d7e5bbd1e18c95defd7b543eb94"
 
@@ -42,62 +41,3 @@ instance (priority := 100) LinearOrderedField.toLinearOrderedSemifield [LinearOr
   { LinearOrderedRing.toLinearOrderedSemiring, ‹LinearOrderedField α› with }
 #align linear_ordered_field.to_linear_ordered_semifield LinearOrderedField.toLinearOrderedSemifield
 
-variable [LinearOrderedSemifield α] {a b : α}
-
-@[simp] lemma inv_pos : 0 < a⁻¹ ↔ 0 < a :=
-  suffices ∀ a : α, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
-  fun a ha ↦ flip lt_of_mul_lt_mul_left ha.le <| by simp [ne_of_gt ha, zero_lt_one]
-#align inv_pos inv_pos
-
-alias ⟨_, inv_pos_of_pos⟩ := inv_pos
-#align inv_pos_of_pos inv_pos_of_pos
-
-@[simp] lemma inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a := by simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]
-#align inv_nonneg inv_nonneg
-
-alias ⟨_, inv_nonneg_of_nonneg⟩ := inv_nonneg
-#align inv_nonneg_of_nonneg inv_nonneg_of_nonneg
-
-@[simp] lemma inv_lt_zero : a⁻¹ < 0 ↔ a < 0 := by simp only [← not_le, inv_nonneg]
-#align inv_lt_zero inv_lt_zero
-
-@[simp] lemma inv_nonpos : a⁻¹ ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, inv_pos]
-#align inv_nonpos inv_nonpos
-
-lemma one_div_pos : 0 < 1 / a ↔ 0 < a := inv_eq_one_div a ▸ inv_pos
-#align one_div_pos one_div_pos
-
-lemma one_div_neg : 1 / a < 0 ↔ a < 0 := inv_eq_one_div a ▸ inv_lt_zero
-#align one_div_neg one_div_neg
-
-lemma one_div_nonneg : 0 ≤ 1 / a ↔ 0 ≤ a := inv_eq_one_div a ▸ inv_nonneg
-#align one_div_nonneg one_div_nonneg
-
-lemma one_div_nonpos : 1 / a ≤ 0 ↔ a ≤ 0 := inv_eq_one_div a ▸ inv_nonpos
-#align one_div_nonpos one_div_nonpos
-
-lemma div_pos (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by
-  rw [div_eq_mul_inv]; exact mul_pos ha (inv_pos.2 hb)
-#align div_pos div_pos
-
-lemma div_nonneg (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by
-  rw [div_eq_mul_inv]; exact mul_nonneg ha (inv_nonneg.2 hb)
-#align div_nonneg div_nonneg
-
-lemma div_nonpos_of_nonpos_of_nonneg (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0 := by
-  rw [div_eq_mul_inv]; exact mul_nonpos_of_nonpos_of_nonneg ha (inv_nonneg.2 hb)
-#align div_nonpos_of_nonpos_of_nonneg div_nonpos_of_nonpos_of_nonneg
-
-lemma div_nonpos_of_nonneg_of_nonpos (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0 := by
-  rw [div_eq_mul_inv]; exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)
-#align div_nonpos_of_nonneg_of_nonpos div_nonpos_of_nonneg_of_nonpos
-
-lemma zpow_nonneg (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
-  | (n : ℕ) => by rw [zpow_natCast]; exact pow_nonneg ha _
-  | -(n + 1 : ℕ) => by rw [zpow_neg, inv_nonneg, zpow_natCast]; exact pow_nonneg ha _
-#align zpow_nonneg zpow_nonneg
-
-lemma zpow_pos_of_pos (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
-  | (n : ℕ) => by rw [zpow_natCast]; exact pow_pos ha _
-  | -(n + 1 : ℕ) => by rw [zpow_neg, inv_pos, zpow_natCast]; exact pow_pos ha _
-#align zpow_pos_of_pos zpow_pos_of_pos

Mathlib/Algebra/Order/Field/Unbundled/Basic.lean

@@ -0,0 +1,81 @@
+/-
+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
+-/
+import Mathlib.Algebra.Field.Defs
+import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Algebra.Order.Ring.Unbundled.Basic
+
+#align_import algebra.order.field.defs from "leanprover-community/mathlib"@"655994e298904d7e5bbd1e18c95defd7b543eb94"
+
+/-!
+# Basic facts for unbundled linear ordered (semi)fields
+
+-/
+
+-- Guard against import creep.
+assert_not_exists OrderedCommMonoid
+assert_not_exists MonoidHom
+
+variable {α : Type*}
+
+variable [Semifield α] [LinearOrder α] [PosMulReflectLT α] [ZeroLEOneClass α] {a b : α}
+
+@[simp] lemma inv_pos : 0 < a⁻¹ ↔ 0 < a :=
+  suffices ∀ a : α, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
+  fun a ha ↦ flip lt_of_mul_lt_mul_left ha.le <| by simp [ne_of_gt ha, zero_lt_one]
+#align inv_pos inv_pos
+
+alias ⟨_, inv_pos_of_pos⟩ := inv_pos
+#align inv_pos_of_pos inv_pos_of_pos
+
+@[simp] lemma inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a := by simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]
+#align inv_nonneg inv_nonneg
+
+alias ⟨_, inv_nonneg_of_nonneg⟩ := inv_nonneg
+#align inv_nonneg_of_nonneg inv_nonneg_of_nonneg
+
+@[simp] lemma inv_lt_zero : a⁻¹ < 0 ↔ a < 0 := by simp only [← not_le, inv_nonneg]
+#align inv_lt_zero inv_lt_zero
+
+@[simp] lemma inv_nonpos : a⁻¹ ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, inv_pos]
+#align inv_nonpos inv_nonpos
+
+lemma one_div_pos : 0 < 1 / a ↔ 0 < a := inv_eq_one_div a ▸ inv_pos
+#align one_div_pos one_div_pos
+
+lemma one_div_neg : 1 / a < 0 ↔ a < 0 := inv_eq_one_div a ▸ inv_lt_zero
+#align one_div_neg one_div_neg
+
+lemma one_div_nonneg : 0 ≤ 1 / a ↔ 0 ≤ a := inv_eq_one_div a ▸ inv_nonneg
+#align one_div_nonneg one_div_nonneg
+
+lemma one_div_nonpos : 1 / a ≤ 0 ↔ a ≤ 0 := inv_eq_one_div a ▸ inv_nonpos
+#align one_div_nonpos one_div_nonpos
+
+lemma div_pos [PosMulStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by
+  rw [div_eq_mul_inv]; exact mul_pos ha (inv_pos.2 hb)
+#align div_pos div_pos
+
+lemma div_nonneg [PosMulMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by
+  rw [div_eq_mul_inv]; exact mul_nonneg ha (inv_nonneg.2 hb)
+#align div_nonneg div_nonneg
+
+lemma div_nonpos_of_nonpos_of_nonneg [MulPosMono α] (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0 := by
+  rw [div_eq_mul_inv]; exact mul_nonpos_of_nonpos_of_nonneg ha (inv_nonneg.2 hb)
+#align div_nonpos_of_nonpos_of_nonneg div_nonpos_of_nonpos_of_nonneg
+
+lemma div_nonpos_of_nonneg_of_nonpos [PosMulMono α] (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0 := by
+  rw [div_eq_mul_inv]; exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)
+#align div_nonpos_of_nonneg_of_nonpos div_nonpos_of_nonneg_of_nonpos
+
+lemma zpow_nonneg [PosMulMono α] (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
+  | (n : ℕ) => by rw [zpow_natCast]; exact pow_nonneg ha _
+  | -(n + 1 : ℕ) => by rw [zpow_neg, inv_nonneg, zpow_natCast]; exact pow_nonneg ha _
+#align zpow_nonneg zpow_nonneg
+
+lemma zpow_pos_of_pos [PosMulStrictMono α] (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
+  | (n : ℕ) => by rw [zpow_natCast]; exact pow_pos ha _
+  | -(n + 1 : ℕ) => by rw [zpow_neg, inv_pos, zpow_natCast]; exact pow_pos ha _
+#align zpow_pos_of_pos zpow_pos_of_pos

Mathlib/Algebra/Order/Module/Defs.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import Mathlib.Algebra.Order.Module.Synonym
 import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.Tactic.Positivity.Core
+import Mathlib.Algebra.Order.Field.Unbundled.Basic
 
 /-!
 # Monotonicity of scalar multiplication by positive elements
@@ -995,13 +996,14 @@ variable [LinearOrderedSemifield α] [AddCommGroup β] [PartialOrder β]
 -- See note [lower instance priority]
 instance (priority := 100) PosSMulMono.toPosSMulReflectLE [MulAction α β] [PosSMulMono α β] :
     PosSMulReflectLE α β where
-  elim _a ha b₁ b₂ h := by simpa [ha.ne'] using smul_le_smul_of_nonneg_left h <| inv_nonneg.2 ha.le
+  elim _a ha b₁ b₂ h := by
+    simpa [ha.ne'] using smul_le_smul_of_nonneg_left h <| inv_nonneg (α := α) |>.2 ha.le
 
 -- See note [lower instance priority]
 instance (priority := 100) PosSMulStrictMono.toPosSMulReflectLT [MulActionWithZero α β]
     [PosSMulStrictMono α β] : PosSMulReflectLT α β :=
   PosSMulReflectLT.of_pos fun a ha b₁ b₂ h ↦ by
-    simpa [ha.ne'] using smul_lt_smul_of_pos_left h <| inv_pos.2 ha
+    simpa [ha.ne'] using smul_lt_smul_of_pos_left h <| inv_pos (α := α) |>.2 ha
 
 end LinearOrderedSemifield