[Merged by Bors] - chore: Move basic ordered field lemmas

Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean

@@ -5,7 +5,6 @@ Authors: Kevin Kappelmann
 -/
 import Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
 import Mathlib.Algebra.ContinuedFractions.TerminatedStable
-import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Ring
 

Mathlib/Algebra/GeomSum.lean

@@ -6,8 +6,9 @@ Authors: Neil Strickland
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.BigOperators.Intervals
-import Mathlib.Tactic.Abel
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Data.Nat.Parity
+import Mathlib.Tactic.Abel
 
 #align_import algebra.geom_sum from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c"
 

Mathlib/Algebra/Order/Field/Basic.lean

@@ -41,90 +41,6 @@ def OrderIso.mulRight₀ (a : α) (ha : 0 < a) : α ≃o α :=
 #align order_iso.mul_right₀_symm_apply OrderIso.mulRight₀_symm_apply
 #align order_iso.mul_right₀_apply OrderIso.mulRight₀_apply
 
-/-!
-### Lemmas about pos, nonneg, nonpos, neg
--/
-
-
-@[simp]
-theorem 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]
-theorem 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]
-theorem inv_lt_zero : a⁻¹ < 0 ↔ a < 0 := by simp only [← not_le, inv_nonneg]
-#align inv_lt_zero inv_lt_zero
-
-@[simp]
-theorem inv_nonpos : a⁻¹ ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, inv_pos]
-#align inv_nonpos inv_nonpos
-
-theorem one_div_pos : 0 < 1 / a ↔ 0 < a :=
-  inv_eq_one_div a ▸ inv_pos
-#align one_div_pos one_div_pos
-
-theorem one_div_neg : 1 / a < 0 ↔ a < 0 :=
-  inv_eq_one_div a ▸ inv_lt_zero
-#align one_div_neg one_div_neg
-
-theorem one_div_nonneg : 0 ≤ 1 / a ↔ 0 ≤ a :=
-  inv_eq_one_div a ▸ inv_nonneg
-#align one_div_nonneg one_div_nonneg
-
-theorem one_div_nonpos : 1 / a ≤ 0 ↔ a ≤ 0 :=
-  inv_eq_one_div a ▸ inv_nonpos
-#align one_div_nonpos one_div_nonpos
-
-theorem 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
-
-theorem 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
-
-theorem 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
-
-theorem 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
-
-theorem zpow_nonneg (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
-  | (n : ℕ) => by
-    rw [zpow_coe_nat]
-    exact pow_nonneg ha _
-  | -(n + 1 : ℕ) => by
-    rw [zpow_neg, inv_nonneg, zpow_coe_nat]
-    exact pow_nonneg ha _
-#align zpow_nonneg zpow_nonneg
-
-theorem zpow_pos_of_pos (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
-  | (n : ℕ) => by
-    rw [zpow_coe_nat]
-    exact pow_pos ha _
-  | -(n + 1 : ℕ) => by
-    rw [zpow_neg, inv_pos, zpow_coe_nat]
-    exact pow_pos ha _
-#align zpow_pos_of_pos zpow_pos_of_pos
-
 /-!
 ### Relating one division with another term.
 -/

Mathlib/Algebra/Order/Field/Defs.lean

@@ -4,6 +4,7 @@ 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.Units.Basic
 import Mathlib.Algebra.Order.Ring.Defs
 
 #align_import algebra.order.field.defs from "leanprover-community/mathlib"@"655994e298904d7e5bbd1e18c95defd7b543eb94"
@@ -20,14 +21,10 @@ A linear ordered (semi)field is a (semi)field equipped with a linear order such
 
 * `LinearOrderedSemifield`: Typeclass for linear order semifields.
 * `LinearOrderedField`: Typeclass for linear ordered fields.
-
-## Implementation details
-
-For olean caching reasons, this file is separate to the main file,
-`Mathlib.Algebra.Order.Field.Basic`. The lemmata are instead located there.
-
 -/
 
+-- Guard against import creep.
+assert_not_exists MonoidHom
 
 variable {α : Type*}
 
@@ -45,5 +42,62 @@ instance (priority := 100) LinearOrderedField.toLinearOrderedSemifield [LinearOr
   { LinearOrderedRing.toLinearOrderedSemiring, ‹LinearOrderedField α› with }
 #align linear_ordered_field.to_linear_ordered_semifield LinearOrderedField.toLinearOrderedSemifield
 
--- Guard against import creep.
-assert_not_exists MonoidHom
+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_coe_nat]; exact pow_nonneg ha _
+  | -(n + 1 : ℕ) => by rw [zpow_neg, inv_nonneg, zpow_coe_nat]; 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_coe_nat]; exact pow_pos ha _
+  | -(n + 1 : ℕ) => by rw [zpow_neg, inv_pos, zpow_coe_nat]; exact pow_pos ha _
+#align zpow_pos_of_pos zpow_pos_of_pos

Mathlib/Algebra/Order/Module/Pointwise.lean

@@ -3,8 +3,9 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Algebra.Order.Module.Defs
+import Mathlib.Data.Set.Pointwise.SMul
+import Mathlib.Order.Bounds.OrderIso
 
 /-!
 # Bounds on scalar multiplication of set

Mathlib/Algebra/Order/Monovary.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.Instances
 import Mathlib.Algebra.Order.Module.OrderedSMul

Mathlib/Algebra/Order/Nonneg/Field.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Field.Canonical.Defs
 import Mathlib.Algebra.Order.Field.InjSurj
 import Mathlib.Algebra.Order.Nonneg.Ring

Mathlib/Algebra/Order/Positive/Field.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.Positive.Ring
 
 #align_import algebra.order.positive.field from "leanprover-community/mathlib"@"bbeb185db4ccee8ed07dc48449414ebfa39cb821"

Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean

@@ -5,9 +5,8 @@ Authors: Yaël Dillies, Vladimir Ivanov
 -/
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.Order
-import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Data.Finset.Sups
-import Mathlib.Order.Hom.Lattice
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Ring
 

Mathlib/Combinatorics/SimpleGraph/Density.lean

@@ -3,13 +3,13 @@ Copyright (c) 2022 Yaël Dillies, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Combinatorics.SimpleGraph.Basic
-import Mathlib.Order.Partition.Finpartition
 import Mathlib.Data.Rat.Cast.Order
-import Mathlib.Tactic.Ring
-import Mathlib.Tactic.NormNum
+import Mathlib.Order.Partition.Finpartition
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 #align_import combinatorics.simple_graph.density from "leanprover-community/mathlib"@"a4ec43f53b0bd44c697bcc3f5a62edd56f269ef1"
 

Mathlib/Data/NNRat/Lemmas.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.Function.Indicator
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Nonneg.Field
 import Mathlib.Data.NNRat.Defs
 import Mathlib.Data.Rat.Field

Mathlib/Data/Rat/Cast/Order.lean

@@ -3,9 +3,9 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
-import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Data.Rat.Cast.CharZero
 import Mathlib.Data.Rat.Order
+import Mathlib.Tactic.Positivity.Core
 
 #align_import data.rat.cast from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
 

Mathlib/NumberTheory/ADEInequality.lean

@@ -3,10 +3,11 @@ Copyright (c) 2021 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Data.Multiset.Sort
+import Mathlib.Data.PNat.Basic
 import Mathlib.Data.PNat.Interval
 import Mathlib.Data.Rat.Order
-import Mathlib.Data.PNat.Basic
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.IntervalCases
 

Mathlib/NumberTheory/Harmonic/Defs.lean

@@ -6,8 +6,8 @@ Authors: Koundinya Vajjha, Thomas Browning
 
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Tactic.Linarith
-import Mathlib.Data.Nat.Interval
 
 /-!
 

Mathlib/Order/Filter/AtTopBot.lean

@@ -3,14 +3,14 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov, Patrick Massot
 -/
-import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Algebra.Order.Field.Defs
+import Mathlib.Algebra.Order.Group.Instances
+import Mathlib.Algebra.Order.Group.MinMax
 import Mathlib.Data.Finset.Preimage
 import Mathlib.Data.Set.Intervals.Disjoint
 import Mathlib.Data.Set.Intervals.OrderIso
-import Mathlib.Order.Filter.Bases
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
-import Mathlib.Algebra.Order.Group.MinMax
-import Mathlib.Algebra.Order.Group.Instances
+import Mathlib.Order.Filter.Bases
 
 #align_import order.filter.at_top_bot from "leanprover-community/mathlib"@"1f0096e6caa61e9c849ec2adbd227e960e9dff58"
 

Mathlib/Order/RelSeries.lean

@@ -3,12 +3,13 @@ Copyright (c) 2023 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Fangming Li
 -/
+import Mathlib.Algebra.Order.WithZero
 import Mathlib.Data.Int.Basic
 import Mathlib.Data.List.Chain
 import Mathlib.Data.List.OfFn
 import Mathlib.Data.Rel
-import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Abel
+import Mathlib.Tactic.Linarith
 
 /-!
 # Series of a relation

Mathlib/Tactic/CancelDenoms/Core.lean

@@ -3,7 +3,8 @@ Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
-import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Algebra.Field.Basic
+import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Data.Tree
 import Mathlib.Logic.Basic
 import Mathlib.Tactic.NormNum.Core

Mathlib/Topology/UniformSpace/AbsoluteValue.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
 import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Topology.UniformSpace.Basic
 
 #align_import topology.uniform_space.absolute_value from "leanprover-community/mathlib"@"e1a7bdeb4fd826b7e71d130d34988f0a2d26a177"

scripts/noshake.json

@@ -297,6 +297,7 @@
    "Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic"],
   "Mathlib.Order.Filter.ListTraverse":
   ["Mathlib.Control.Traversable.Instances"],
+  "Mathlib.NumberTheory.Harmonic.Defs": ["Mathlib.Algebra.Order.Field.Basic"],
   "Mathlib.NumberTheory.ArithmeticFunction": ["Mathlib.Tactic.ArithMult"],
   "Mathlib.Logic.Nontrivial.Defs": ["Mathlib.Init.Logic"],
   "Mathlib.Logic.Equiv.Defs": ["Mathlib.Init.Data.Bool.Lemmas"],
@@ -320,6 +321,8 @@
   "Mathlib.Control.Traversable.Instances": ["Mathlib.Control.Applicative"],
   "Mathlib.Control.Monad.Basic": ["Mathlib.Init.Control.Lawful"],
   "Mathlib.Control.Basic": ["Mathlib.Init.Function"],
+  "Mathlib.Combinatorics.SetFamily.AhlswedeZhang":
+  ["Mathlib.Algebra.Order.Field.Basic"],
   "Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits":
   ["Mathlib.CategoryTheory.Limits.Shapes.Pullbacks"],
   "Mathlib.AlgebraicTopology.DoldKan.Notations":
@@ -334,4 +337,4 @@
   "Mathlib.Algebra.Category.Ring.Basic":
   ["Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso"],
   "Mathlib.Algebra.Algebra.Subalgebra.Order":
-  ["Mathlib.Algebra.Module.Submodule.Order"]}}
+  ["Mathlib.Algebra.Module.Submodule.Order"]}}

test/GCongr/inequalities.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
 import Mathlib.Algebra.BigOperators.Order
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Parity
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.GCongr