[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/Combinatorics/Additive/PluenneckeRuzsa.lean

@@ -5,7 +5,7 @@ Authors: Yaël Dillies, George Shakan
 -/
 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
 

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
 
@@ -31,14 +30,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 +44,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 +126,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 +200,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 +331,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 +387,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,95 @@
+/-
+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
+
+#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
+
+instance instDenselyOrdered : DenselyOrdered NNRat := Nonneg.densely_ordered
+
+namespace NNRat
+variable {α : Type*} {p q : ℚ≥0}
+
+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