chore(NNRat): Rearrange imports (#10392)

The goal is to separate the field material on `Rat`/`NNRat` from everything before to make way for `NNRat.cast`. We achieve this by
* splitting `Data.Rat.NNRat` into
  * `Data.NNRat.Defs` for the foundationl stuff that will be needed in the definition of `Field`
  * `Data.NNRat.Lemmas` for the field and big operators material
* moving the field material from `Data.Rat.Order` to `Data.Rat.Basic`
* proving a few lemmas by `rfl` rather than `coeHom.some_now_unavailable_lemma`
* renaming `Data.Rat.NNRat.BigOperators` to `Data.NNRat.BigOperators`

Author: YaelDillies

Mathlib.lean

@@ -1794,6 +1794,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
@@ -1942,7 +1945,6 @@ import Mathlib.Data.QPF.Multivariate.Constructions.Quot
 import Mathlib.Data.QPF.Multivariate.Constructions.Sigma
 import Mathlib.Data.QPF.Univariate.Basic
 import Mathlib.Data.Quot
-import Mathlib.Data.Rat.Basic
 import Mathlib.Data.Rat.BigOperators
 import Mathlib.Data.Rat.Cast.CharZero
 import Mathlib.Data.Rat.Cast.Defs
@@ -1951,11 +1953,10 @@ import Mathlib.Data.Rat.Cast.Order
 import Mathlib.Data.Rat.Defs
 import Mathlib.Data.Rat.Denumerable
 import Mathlib.Data.Rat.Encodable
+import Mathlib.Data.Rat.Field
 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 @@ Authors: Yaël Dillies, George Shakan
 -/
 import Mathlib.Combinatorics.DoubleCounting
 import Mathlib.Data.Finset.Pointwise
-import Mathlib.Data.Rat.NNRat
+import Mathlib.Data.NNRat.Lemmas
 import Mathlib.Tactic.GCongr
 import Mathlib.Algebra.GroupPower.Order
 

Mathlib/Data/Rat/NNRat/BigOperators.lean renamed to 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 renamed to 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 that 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,7 @@ 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
+
+-- `NNRat` needs to be available in the definition of `Field`
+assert_not_exists Field

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
+import Mathlib.Data.Rat.Field
+
+#align_import data.rat.nnrat from "leanprover-community/mathlib"@"b3f4f007a962e3787aa0f3b5c7942a1317f7d88e"
+
+/-!
+# Field and action 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
+
+-- The `LinearOrderedCommGroupWithZero` instance is a shortcut instance for performance
+deriving instance CanonicallyLinearOrderedSemifield, LinearOrderedCommGroupWithZero for NNRat
+
+namespace NNRat
+variable {α : Type*} {p q : ℚ≥0}
+
+instance instDenselyOrdered : DenselyOrdered ℚ≥0 := Nonneg.instDenselyOrdered
+
+@[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/Cast/Defs.lean

@@ -3,7 +3,7 @@ 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.Data.Rat.Basic
+import Mathlib.Data.Rat.Field
 import Mathlib.Data.Rat.Lemmas
 
 #align_import data.rat.cast from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"

Mathlib/Data/Rat/Basic.lean renamed to Mathlib/Data/Rat/Field.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