[Merged by Bors] - chore(NNRat): Rearrange imports

Mathlib.lean

@@ -1788,6 +1788,9 @@ import Mathlib.Data.MvPolynomial.Polynomial
 import Mathlib.Data.MvPolynomial.Rename
 import Mathlib.Data.MvPolynomial.Supported
 import Mathlib.Data.MvPolynomial.Variables
+import Mathlib.Data.NNRat.BigOperators
+import Mathlib.Data.NNRat.Defs
+import Mathlib.Data.NNRat.Lemmas
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Bits
 import Mathlib.Data.Nat.Bitwise
@@ -1948,8 +1951,6 @@ import Mathlib.Data.Rat.Encodable
 import Mathlib.Data.Rat.Floor
 import Mathlib.Data.Rat.Init
 import Mathlib.Data.Rat.Lemmas
-import Mathlib.Data.Rat.NNRat
-import Mathlib.Data.Rat.NNRat.BigOperators
 import Mathlib.Data.Rat.Order
 import Mathlib.Data.Rat.Sqrt
 import Mathlib.Data.Rat.Star

Mathlib/Algebra/Module/Basic.lean

@@ -6,7 +6,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.Data.Int.Basic
-import Mathlib.Data.Rat.NNRat
+import Mathlib.Data.NNRat.Defs
 import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.GroupTheory.GroupAction.Pi
 import Mathlib.Logic.Basic

Mathlib/Algebra/Order/Archimedean.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.GroupPower.Order
 import Mathlib.Algebra.Order.Field.Power
 import Mathlib.Data.Int.LeastGreatest
 import Mathlib.Data.Rat.Floor
-import Mathlib.Data.Rat.NNRat
+import Mathlib.Data.NNRat.Defs
 
 #align_import algebra.order.archimedean from "leanprover-community/mathlib"@"6f413f3f7330b94c92a5a27488fdc74e6d483a78"
 

Mathlib/Algebra/Order/Nonneg/Ring.lean

@@ -70,10 +70,10 @@ instance distribLattice [DistribLattice α] {a : α} : DistribLattice { x : α /
   Set.Ici.distribLattice
 #align nonneg.distrib_lattice Nonneg.distribLattice
 
-instance densely_ordered [Preorder α] [DenselyOrdered α] {a : α} :
+instance instDenselyOrdered [Preorder α] [DenselyOrdered α] {a : α} :
     DenselyOrdered { x : α // a ≤ x } :=
   show DenselyOrdered (Ici a) from Set.instDenselyOrdered
-#align nonneg.densely_ordered Nonneg.densely_ordered
+#align nonneg.densely_ordered Nonneg.instDenselyOrdered
 
 /-- If `sSup ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrder`. -/
 @[reducible]

Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

@@ -5,7 +5,7 @@
 -/
 import Mathlib.Combinatorics.DoubleCounting
 import Mathlib.Data.Finset.Pointwise
-import Mathlib.Data.Rat.NNRat
+import Mathlib.Data.NNRat.Defs
 import Mathlib.Tactic.GCongr
 import Mathlib.Algebra.GroupPower.Order
 
@@ -123,16 +123,16 @@
 -- Auxiliary lemma for Ruzsa's triangle sum inequality, and the Plünnecke-Ruzsa inequality.
 @[to_additive]
 private theorem mul_aux (hA : A.Nonempty) (hAB : A ⊆ B)
     (h : ∀ A' ∈ B.powerset.erase ∅, ((A * C).card : ℚ≥0) / ↑A.card ≤ (A' * C).card / ↑A'.card) :
     ∀ A' ⊆ A, (A * C).card * A'.card ≤ (A' * C).card * A.card := by
   rintro A' hAA'
   obtain rfl | hA' := A'.eq_empty_or_nonempty
   · simp
   have hA₀ : (0 : ℚ≥0) < A.card := cast_pos.2 hA.card_pos
   have hA₀' : (0 : ℚ≥0) < A'.card := cast_pos.2 hA'.card_pos
   exact mod_cast
     (div_le_div_iff hA₀ hA₀').1
       (h _ <| mem_erase_of_ne_of_mem hA'.ne_empty <| mem_powerset.2 <| hAA'.trans hAB)
 
 /-- **Ruzsa's triangle inequality**. Multiplication version. -/
 @[to_additive card_add_mul_card_le_card_add_mul_card_add
@@ -145,9 +145,9 @@
   obtain ⟨U, hU, hUA⟩ :=
     exists_min_image (B.powerset.erase ∅) (fun U ↦ (U * A).card / U.card : _ → ℚ≥0) ⟨B, hB'⟩
   rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hU
   refine' cast_le.1 (_ : (_ : ℚ≥0) ≤ _)
   push_cast
   refine' (le_div_iff <| cast_pos.2 hB.card_pos).1 _
   rw [mul_div_right_comm, mul_comm _ B]
   refine' (cast_le.2 <| card_le_card_mul_left _ hU.1).trans _
   refine' le_trans _
@@ -187,7 +187,7 @@
   · simp
   induction' n with n ih
   · simp
   rw [succ_nsmul, ← add_assoc, _root_.pow_succ, mul_assoc, ← mul_div_right_comm, le_div_iff,
     ← cast_mul]
   swap; exact cast_pos.2 hA.card_pos
   refine' (cast_le.2 <| add_pluennecke_petridis _ hAB).trans _
@@ -202,7 +202,7 @@
   · simp
   induction' n with n ih
   · simp
   rw [_root_.pow_succ, ← mul_assoc, _root_.pow_succ, @mul_assoc ℚ≥0, ← mul_div_right_comm,
     le_div_iff, ← cast_mul]
   swap; exact cast_pos.2 hA.card_pos
   refine' (cast_le.2 <| mul_pluennecke_petridis _ hAB).trans _
@@ -220,7 +220,7 @@
   obtain ⟨C, hC, hCA⟩ :=
     exists_min_image (A.powerset.erase ∅) (fun C ↦ (C * B).card / C.card : _ → ℚ≥0) ⟨A, hA'⟩
   rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hC
   refine' (mul_le_mul_right <| cast_pos.2 hC.1.card_pos).1 _
   norm_cast
   refine' (cast_le.2 <| card_div_mul_le_card_mul_mul_card_mul _ _ _).trans _
   push_cast

Mathlib/Data/Rat/NNRat/BigOperators.lean → Mathlib/Data/NNRat/BigOperators.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.BigOperators.Order
-import Mathlib.Data.Rat.NNRat
+import Mathlib.Data.NNRat.Defs
 
 /-! # Casting lemmas for non-negative rational numbers involving sums and products
 -/

Mathlib/Data/Rat/NNRat.lean → Mathlib/Data/NNRat/Defs.lean

@@ -3,8 +3,7 @@ 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.Function.Indicator
-import Mathlib.Algebra.Order.Nonneg.Field
+import Mathlib.Algebra.Order.Nonneg.Ring
 import Mathlib.Data.Int.Lemmas
 import Mathlib.Data.Rat.Order
 
@@ -13,8 +12,10 @@ import Mathlib.Data.Rat.Order
 /-!
 # Nonnegative rationals
 
-This file defines the nonnegative rationals as a subtype of `Rat` and provides its algebraic order
-structure.
+This file defines the nonnegative rationals as a subtype of `Rat` and provides its basic algebraic
+order structure.
+
+Note that `NNRat` is not declared as a `Field` here. See `Data.NNRat.Lemmas` for the instance.
 
 We also define an instance `CanLift ℚ ℚ≥0`. This instance can be used by the `lift` tactic to
 replace `x : ℚ` and `hx : 0 ≤ x` in the proof context with `x : ℚ≥0` while replacing all occurrences
@@ -31,14 +32,12 @@ open Function
 
 /-- Nonnegative rational numbers. -/
 def NNRat := { q : ℚ // 0 ≤ q } deriving
-  CanonicallyOrderedCommSemiring, CanonicallyLinearOrderedSemifield, LinearOrderedCommGroupWithZero,
-  Sub, Inhabited
+  CanonicallyOrderedCommSemiring, CanonicallyLinearOrderedAddCommMonoid, Sub, Inhabited
 #align nnrat NNRat
 
 -- Porting note: Added these instances to get `OrderedSub, DenselyOrdered, Archimedean`
 -- instead of `deriving` them
 instance : OrderedSub NNRat := Nonneg.orderedSub
-instance : DenselyOrdered NNRat := Nonneg.densely_ordered
 
 -- mathport name: nnrat
 scoped[NNRat] notation "ℚ≥0" => NNRat
@@ -47,8 +46,7 @@ namespace NNRat
 
 variable {α : Type*} {p q : ℚ≥0}
 
-instance : Coe ℚ≥0 ℚ :=
-  ⟨Subtype.val⟩
+instance instCoe : Coe ℚ≥0 ℚ := ⟨Subtype.val⟩
 
 /-
 -- Simp lemma to put back `n.val` into the normal form given by the coercion.
@@ -130,16 +128,6 @@ theorem coe_mul (p q : ℚ≥0) : ((p * q : ℚ≥0) : ℚ) = p * q :=
   rfl
 #align nnrat.coe_mul NNRat.coe_mul
 
-@[simp, norm_cast]
-theorem coe_inv (q : ℚ≥0) : ((q⁻¹ : ℚ≥0) : ℚ) = (q : ℚ)⁻¹ :=
-  rfl
-#align nnrat.coe_inv NNRat.coe_inv
-
-@[simp, norm_cast]
-theorem coe_div (p q : ℚ≥0) : ((p / q : ℚ≥0) : ℚ) = p / q :=
-  rfl
-#align nnrat.coe_div NNRat.coe_div
-
 -- Porting note: `bit0` `bit1` are deprecated, so remove these theorems.
 #noalign nnrat.coe_bit0
 #noalign nnrat.coe_bit1
@@ -214,25 +202,11 @@ theorem mk_coe_nat (n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), n.cast_nonneg⟩ : ℚ
   ext (coe_natCast n).symm
 #align nnrat.mk_coe_nat NNRat.mk_coe_nat
 
-/-- A `MulAction` over `ℚ` restricts to a `MulAction` over `ℚ≥0`. -/
-instance [MulAction ℚ α] : MulAction ℚ≥0 α :=
-  MulAction.compHom α coeHom.toMonoidHom
-
-/-- A `DistribMulAction` over `ℚ` restricts to a `DistribMulAction` over `ℚ≥0`. -/
-instance [AddCommMonoid α] [DistribMulAction ℚ α] : DistribMulAction ℚ≥0 α :=
-  DistribMulAction.compHom α coeHom.toMonoidHom
-
 @[simp]
 theorem coe_coeHom : ⇑coeHom = ((↑) : ℚ≥0 → ℚ) :=
   rfl
 #align nnrat.coe_coe_hom NNRat.coe_coeHom
 
-@[simp, norm_cast]
-theorem coe_indicator (s : Set α) (f : α → ℚ≥0) (a : α) :
-    ((s.indicator f a : ℚ≥0) : ℚ) = s.indicator (fun x ↦ ↑(f x)) a :=
-  (coeHom : ℚ≥0 →+ ℚ).map_indicator _ _ _
-#align nnrat.coe_indicator NNRat.coe_indicator
-
 @[simp, norm_cast]
 theorem coe_pow (q : ℚ≥0) (n : ℕ) : (↑(q ^ n) : ℚ) = (q : ℚ) ^ n :=
   coeHom.map_pow _ _
@@ -359,21 +333,6 @@ theorem toNNRat_mul (hp : 0 ≤ p) : toNNRat (p * q) = toNNRat p * toNNRat q :=
     rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]
 #align rat.to_nnrat_mul Rat.toNNRat_mul
 
-theorem toNNRat_inv (q : ℚ) : toNNRat q⁻¹ = (toNNRat q)⁻¹ := by
-  obtain hq | hq := le_total q 0
-  · rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]
-  · nth_rw 1 [← Rat.coe_toNNRat q hq]
-    rw [← coe_inv, toNNRat_coe]
-#align rat.to_nnrat_inv Rat.toNNRat_inv
-
-theorem toNNRat_div (hp : 0 ≤ p) : toNNRat (p / q) = toNNRat p / toNNRat q := by
-  rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]
-#align rat.to_nnrat_div Rat.toNNRat_div
-
-theorem toNNRat_div' (hq : 0 ≤ q) : toNNRat (p / q) = toNNRat p / toNNRat q := by
-  rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]
-#align rat.to_nnrat_div' Rat.toNNRat_div'
-
 end Rat
 
 /-- The absolute value on `ℚ` as a map to `ℚ≥0`. -/
@@ -430,18 +389,4 @@ theorem ext_num_den_iff : p = q ↔ p.num = q.num ∧ p.den = q.den :=
   ⟨by rintro rfl; exact ⟨rfl, rfl⟩, fun h ↦ ext_num_den h.1 h.2⟩
 #align nnrat.ext_num_denom_iff NNRat.ext_num_den_iff
 
-@[simp]
-theorem num_div_den (q : ℚ≥0) : (q.num : ℚ≥0) / q.den = q := by
-  ext1
-  rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_ofNat,
-    Int.natAbs_of_nonneg (Rat.num_nonneg_iff_zero_le.2 q.prop)]
-  exact Rat.num_div_den q
-#align nnrat.num_div_denom NNRat.num_div_den
-
-/-- A recursor for nonnegative rationals in terms of numerators and denominators. -/
-protected def rec {α : ℚ≥0 → Sort*} (h : ∀ m n : ℕ, α (m / n)) (q : ℚ≥0) : α q := by
-  rw [← num_div_den q]
-  apply h
-#align nnrat.rec NNRat.rec
-
 end NNRat

Mathlib/Data/NNRat/Lemmas.lean

@@ -0,0 +1,96 @@
+/-
+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.Function.Indicator
+import Mathlib.Algebra.Order.Nonneg.Field
+import Mathlib.Data.NNRat.Defs
+import Mathlib.Data.Rat.Basic
+
+#align_import data.rat.nnrat from "leanprover-community/mathlib"@"b3f4f007a962e3787aa0f3b5c7942a1317f7d88e"
+
+/-!
+# Algebraic structures on the nonnegative rationals
+
+This file provides additional results about `NNRat` that cannot live in earlier files due to import
+cycles.
+-/
+
+open Function
+open scoped NNRat
+
+deriving instance CanonicallyLinearOrderedSemifield, LinearOrderedCommGroupWithZero for NNRat
+
+namespace NNRat
+variable {α : Type*} {p q : ℚ≥0}
+
+instance instDenselyOrdered : DenselyOrdered ℚ≥0 := Nonneg.instDenselyOrdered
+
+open Rat (toNNRat)
+
+@[simp, norm_cast] lemma coe_inv (q : ℚ≥0) : ((q⁻¹ : ℚ≥0) : ℚ) = (q : ℚ)⁻¹ := rfl
+#align nnrat.coe_inv NNRat.coe_inv
+
+@[simp, norm_cast] lemma coe_div (p q : ℚ≥0) : ((p / q : ℚ≥0) : ℚ) = p / q := rfl
+#align nnrat.coe_div NNRat.coe_div
+
+/-- A `MulAction` over `ℚ` restricts to a `MulAction` over `ℚ≥0`. -/
+instance [MulAction ℚ α] : MulAction ℚ≥0 α :=
+  MulAction.compHom α coeHom.toMonoidHom
+
+/-- A `DistribMulAction` over `ℚ` restricts to a `DistribMulAction` over `ℚ≥0`. -/
+instance [AddCommMonoid α] [DistribMulAction ℚ α] : DistribMulAction ℚ≥0 α :=
+  DistribMulAction.compHom α coeHom.toMonoidHom
+
+@[simp, norm_cast]
+lemma coe_indicator (s : Set α) (f : α → ℚ≥0) (a : α) :
+    ((s.indicator f a : ℚ≥0) : ℚ) = s.indicator (fun x ↦ ↑(f x)) a :=
+  (coeHom : ℚ≥0 →+ ℚ).map_indicator _ _ _
+#align nnrat.coe_indicator NNRat.coe_indicator
+
+end NNRat
+
+open NNRat
+
+namespace Rat
+
+variable {p q : ℚ}
+
+lemma toNNRat_inv (q : ℚ) : toNNRat q⁻¹ = (toNNRat q)⁻¹ := by
+  obtain hq | hq := le_total q 0
+  · rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]
+  · nth_rw 1 [← Rat.coe_toNNRat q hq]
+    rw [← coe_inv, toNNRat_coe]
+#align rat.to_nnrat_inv Rat.toNNRat_inv
+
+lemma toNNRat_div (hp : 0 ≤ p) : toNNRat (p / q) = toNNRat p / toNNRat q := by
+  rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]
+#align rat.to_nnrat_div Rat.toNNRat_div
+
+lemma toNNRat_div' (hq : 0 ≤ q) : toNNRat (p / q) = toNNRat p / toNNRat q := by
+  rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]
+#align rat.to_nnrat_div' Rat.toNNRat_div'
+
+end Rat
+
+/-! ### Numerator and denominator -/
+
+namespace NNRat
+
+variable {p q : ℚ≥0}
+
+@[simp]
+lemma num_div_den (q : ℚ≥0) : (q.num : ℚ≥0) / q.den = q := by
+  ext : 1
+  rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_ofNat,
+    Int.natAbs_of_nonneg (Rat.num_nonneg_iff_zero_le.2 q.prop)]
+  exact Rat.num_div_den q
+#align nnrat.num_div_denom NNRat.num_div_den
+
+/-- A recursor for nonnegative rationals in terms of numerators and denominators. -/
+protected def rec {α : ℚ≥0 → Sort*} (h : ∀ m n : ℕ, α (m / n)) (q : ℚ≥0) : α q := by
+  rw [← num_div_den q]; apply h
+#align nnrat.rec NNRat.rec
+
+end NNRat

Mathlib/Data/Rat/Basic.lean

@@ -3,8 +3,8 @@ 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.Field.Defs
-import Mathlib.Data.Rat.Defs
+import Mathlib.Algebra.Order.Field.Defs
+import Mathlib.Data.Rat.Order
 
 #align_import data.rat.basic from "leanprover-community/mathlib"@"a59dad53320b73ef180174aae867addd707ef00e"
 
@@ -45,4 +45,6 @@ instance field : Field ℚ :=
 -- Extra instances to short-circuit type class resolution
 instance divisionRing : DivisionRing ℚ := by infer_instance
 
+instance instLinearOrderedField : LinearOrderedField ℚ := { field, instLinearOrderedCommRing with }
+
 end Rat

Mathlib/Data/Rat/Order.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Init.Data.Bool.Lemmas
-import Mathlib.Algebra.Order.Field.Defs
-import Mathlib.Data.Rat.Basic
+import Mathlib.Data.Rat.Defs
 import Mathlib.Data.Int.Cast.Lemmas
 
 #align_import data.rat.order from "leanprover-community/mathlib"@"a59dad53320b73ef180174aae867addd707ef00e"
@@ -252,17 +251,14 @@ protected theorem mul_nonneg {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a
   rw [← nonneg_iff_zero_le] at ha hb ⊢; exact Rat.nonneg_mul ha hb
 #align rat.mul_nonneg Rat.mul_nonneg
 
-instance : LinearOrderedField ℚ :=
-  { Rat.field, Rat.linearOrder, Rat.semiring with
-    zero_le_one := by decide
-    add_le_add_left := fun a b ab c => Rat.add_le_add_left.2 ab
-    mul_pos := fun a b ha hb =>
-      lt_of_le_of_ne (Rat.mul_nonneg (le_of_lt ha) (le_of_lt hb))
-        (mul_ne_zero (ne_of_lt ha).symm (ne_of_lt hb).symm).symm }
+instance instLinearOrderedCommRing : LinearOrderedCommRing ℚ where
+  __ := Rat.linearOrder
+  __ := Rat.commRing
+  zero_le_one := by decide
+  add_le_add_left := fun a b ab c => Rat.add_le_add_left.2 ab
+  mul_pos a b ha hb := (Rat.mul_nonneg ha.le hb.le).lt_of_ne' (mul_ne_zero ha.ne' hb.ne')
 
 -- Extra instances to short-circuit type class resolution
-instance : LinearOrderedCommRing ℚ := by infer_instance
-
 instance : LinearOrderedRing ℚ := by infer_instance
 
 instance : OrderedRing ℚ := by infer_instance