chore(data/rat/*): Rearrange imports

src/combinatorics/additive/pluennecke_ruzsa.lean

@@ -5,7 +5,6 @@ Authors: Yaël Dillies, George Shakan
 -/
 import combinatorics.double_counting
 import data.finset.pointwise
-import data.rat.nnrat
 
 /-!
 # The Plünnecke-Ruzsa inequality

src/data/rat/basic.lean

@@ -3,8 +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 algebra.field.defs
-import data.rat.defs
+import algebra.order.nonneg.field
+import data.rat.nnrat.defs
+import tactic.nth_rewrite
 
 /-!
 # Field Structure on the Rational Numbers
@@ -33,7 +34,8 @@ hierarchy `data.rat.basic → algebra.field.basic → data.rat.defs`.
 rat, rationals, field, ℚ, numerator, denominator, num, denom
 -/
 
-namespace rat
+
+open_locale nnrat
 
 instance : field ℚ :=
 { zero             := 0,
@@ -43,12 +45,75 @@ instance : field ℚ :=
   mul              := (*),
   inv              := has_inv.inv,
   rat_cast         := id,
-  rat_cast_mk      := λ a b h1 h2, (num_div_denom _).symm,
+  rat_cast_mk      := λ a b h1 h2, (rat.num_div_denom _).symm,
   qsmul            := (*),
   .. rat.comm_ring,
   .. rat.comm_group_with_zero}
 
+instance : linear_ordered_field ℚ := { ..rat.field, ..rat.linear_ordered_comm_ring }
+
 /- Extra instances to short-circuit type class resolution -/
 instance : division_ring ℚ      := by apply_instance
 
+attribute [derive canonically_linear_ordered_semifield] nnrat
+
+namespace nnrat
+variables {p q : ℚ≥0}
+
+@[simp] lemma num_div_denom (q : ℚ≥0) : (q.num : ℚ≥0) / q.denom = q :=
+begin
+  refine ext (_ : ↑((int.nat_abs _ : ℤ)) / _ = _),
+  rw int.nat_abs_of_nonneg (rat.num_nonneg_iff_zero_le.2 q.prop),
+  exact rat.num_div_denom q,
+end
+
+/-- A recursor for nonnegative rationals in terms of numerators and denominators. -/
+protected def rec {α : ℚ≥0 → Sort*} (h : Π m n : ℕ, α (m / n)) (q : ℚ≥0) : α q :=
+(num_div_denom _).rec (h _ _)
+
+lemma add_def (hp : p.denom ≠ 0) (hq : q.denom ≠ 0) :
+  p + q = (p.num * q.denom + p.denom * q.num) / (p.denom * q.denom) :=
+by rw [←div_add_div, num_div_denom, num_div_denom]; rwa nat.cast_ne_zero
+
+lemma mul_def : p * q = (p.num * q.num) / (p.denom * q.denom) :=
+by simp_rw [mul_div_mul_comm, num_div_denom]
+
+end nnrat
+
+namespace nnrat
+variables {α : Type*} {p q : ℚ≥0}
+
+@[simp, norm_cast] lemma coe_inv (q : ℚ≥0) : ((q⁻¹ : ℚ≥0) : ℚ) = q⁻¹ := rfl
+@[simp, norm_cast] lemma coe_div (p q : ℚ≥0) : ((p / q : ℚ≥0) : ℚ) = p / q := rfl
+@[simp, norm_cast] lemma coe_zpow (q : ℚ≥0) (n : ℤ) : (↑(q ^ n) : ℚ) = q ^ n := rfl
+
+/-- A `mul_action` over `ℚ` restricts to a `mul_action` over `ℚ≥0`. -/
+instance [mul_action ℚ α] : mul_action ℚ≥0 α :=
+mul_action.comp_hom α ⟨(coe : ℚ≥0 → ℚ), rfl, λ _ _, rfl⟩
+
+/-- A `distrib_mul_action` over `ℚ` restricts to a `distrib_mul_action` over `ℚ≥0`. -/
+instance [add_comm_monoid α] [distrib_mul_action ℚ α] : distrib_mul_action ℚ≥0 α :=
+distrib_mul_action.comp_hom α ⟨(coe : ℚ≥0 → ℚ), rfl, λ _ _, rfl⟩
+
+end nnrat
+
+open nnrat
+
+namespace rat
+variables {p q : ℚ}
+
+lemma to_nnrat_inv (q : ℚ) : to_nnrat q⁻¹ = (to_nnrat q)⁻¹ :=
+begin
+  obtain hq | hq := le_total q 0,
+  { rw [to_nnrat_eq_zero.mpr hq, inv_zero, to_nnrat_eq_zero.mpr (inv_nonpos.mpr hq)] },
+  { nth_rewrite 0 ←rat.coe_to_nnrat q hq,
+    rw [←coe_inv, to_nnrat_coe] }
+end
+
+lemma to_nnrat_div (hp : 0 ≤ p) : to_nnrat (p / q) = to_nnrat p / to_nnrat q :=
+by rw [div_eq_mul_inv, div_eq_mul_inv, ←to_nnrat_inv, ←to_nnrat_mul hp]
+
+lemma to_nnrat_div' (hq : 0 ≤ q) : to_nnrat (p / q) = to_nnrat p / to_nnrat q :=
+by rw [div_eq_inv_mul, div_eq_inv_mul, to_nnrat_mul (inv_nonneg.2 hq), to_nnrat_inv]
+
 end rat

src/data/rat/cast.lean

@@ -3,12 +3,12 @@ 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 data.rat.order
-import data.rat.lemmas
-import data.int.char_zero
-import algebra.group_with_zero.power
 import algebra.field.opposite
+import algebra.group_with_zero.power
 import algebra.order.field.basic
+import data.int.char_zero
+import data.rat.basic
+import data.rat.lemmas
 
 /-!
 # Casts for Rational Numbers

src/data/rat/nnrat.lean → src/data/rat/nnrat/defs.lean

@@ -3,9 +3,9 @@ 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 algebra.algebra.basic
-import algebra.order.nonneg.field
-import algebra.order.nonneg.floor
+import algebra.order.nonneg.ring
+import data.int.lemmas
+import data.rat.order
 
 /-!
 # Nonnegative rationals
@@ -27,12 +27,10 @@ of `x` with `↑x`. This tactic also works for a function `f : α → ℚ` with
 -/
 
 open function
-open_locale big_operators
 
 /-- Nonnegative rational numbers. -/
-@[derive [canonically_ordered_comm_semiring, canonically_linear_ordered_semifield,
-  linear_ordered_comm_group_with_zero, has_sub, has_ordered_sub,
-  densely_ordered, archimedean, inhabited]]
+@[derive [canonically_ordered_comm_semiring, canonically_linear_ordered_add_monoid, has_sub,
+  has_ordered_sub, inhabited]]
 def nnrat := {q : ℚ // 0 ≤ q}
 
 localized "notation (name := nnrat) `ℚ≥0` := nnrat" in nnrat
@@ -75,12 +73,14 @@ open _root_.rat (to_nnrat)
 @[simp, norm_cast] lemma coe_one  : ((1 : ℚ≥0) : ℚ) = 1 := rfl
 @[simp, norm_cast] lemma coe_add (p q : ℚ≥0) : ((p + q : ℚ≥0) : ℚ) = p + q := rfl
 @[simp, norm_cast] lemma coe_mul (p q : ℚ≥0) : ((p * q : ℚ≥0) : ℚ) = p * q := rfl
-@[simp, norm_cast] lemma coe_inv (q : ℚ≥0) : ((q⁻¹ : ℚ≥0) : ℚ) = q⁻¹ := rfl
-@[simp, norm_cast] lemma coe_div (p q : ℚ≥0) : ((p / q : ℚ≥0) : ℚ) = p / q := rfl
+@[simp, norm_cast] lemma coe_pow (q : ℚ≥0) (n : ℕ) : (↑(q ^ n) : ℚ) = q ^ n := rfl
 @[simp, norm_cast] lemma coe_bit0 (q : ℚ≥0) : ((bit0 q : ℚ≥0) : ℚ) = bit0 q := rfl
 @[simp, norm_cast] lemma coe_bit1 (q : ℚ≥0) : ((bit1 q : ℚ≥0) : ℚ) = bit1 q := rfl
 @[simp, norm_cast] lemma coe_sub (h : q ≤ p) : ((p - q : ℚ≥0) : ℚ) = p - q :=
 max_eq_left $ le_sub_comm.2 $ by simp [show (q : ℚ) ≤ p, from h]
+@[norm_cast] lemma nsmul_coe (q : ℚ≥0) (n : ℕ) : ↑(n • q) = n • (q : ℚ) := rfl
+@[simp, norm_cast] lemma coe_nat_cast (n : ℕ) : (↑(↑n : ℚ≥0) : ℚ) = n := rfl
+@[simp] lemma mk_coe_nat (n : ℕ) : @eq ℚ≥0 (⟨(n : ℚ), n.cast_nonneg⟩ : ℚ≥0) n := rfl
 
 @[simp] lemma coe_eq_zero : (q : ℚ) = 0 ↔ q = 0 := by norm_cast
 lemma coe_ne_zero : (q : ℚ) ≠ 0 ↔ q ≠ 0 := coe_eq_zero.not
@@ -105,67 +105,8 @@ galois_insertion.monotone_intro coe_mono to_nnrat_mono rat.le_coe_to_nnrat to_nn
 /-- Coercion `ℚ≥0 → ℚ` as a `ring_hom`. -/
 def coe_hom : ℚ≥0 →+* ℚ := ⟨coe, coe_one, coe_mul, coe_zero, coe_add⟩
 
-@[simp, norm_cast] lemma coe_nat_cast (n : ℕ) : (↑(↑n : ℚ≥0) : ℚ) = n := map_nat_cast coe_hom n
-
-@[simp] lemma mk_coe_nat (n : ℕ) : @eq ℚ≥0 (⟨(n : ℚ), n.cast_nonneg⟩ : ℚ≥0) n :=
-ext (coe_nat_cast n).symm
-
-/-- The rational numbers are an algebra over the non-negative rationals. -/
-instance : algebra ℚ≥0 ℚ := coe_hom.to_algebra
-
-/-- A `mul_action` over `ℚ` restricts to a `mul_action` over `ℚ≥0`. -/
-instance [mul_action ℚ α] : mul_action ℚ≥0 α := mul_action.comp_hom α coe_hom.to_monoid_hom
-
-/-- A `distrib_mul_action` over `ℚ` restricts to a `distrib_mul_action` over `ℚ≥0`. -/
-instance [add_comm_monoid α] [distrib_mul_action ℚ α] : distrib_mul_action ℚ≥0 α :=
-distrib_mul_action.comp_hom α coe_hom.to_monoid_hom
-
-/-- A `module` over `ℚ` restricts to a `module` over `ℚ≥0`. -/
-instance [add_comm_monoid α] [module ℚ α] : module ℚ≥0 α := module.comp_hom α coe_hom
-
 @[simp] lemma coe_coe_hom : ⇑coe_hom = coe := rfl
 
-@[simp, norm_cast] lemma coe_indicator (s : set α) (f : α → ℚ≥0) (a : α) :
-  ((s.indicator f a : ℚ≥0) : ℚ) = s.indicator (λ x, f x) a :=
-(coe_hom : ℚ≥0 →+ ℚ).map_indicator _ _ _
-
-@[simp, norm_cast] lemma coe_pow (q : ℚ≥0) (n : ℕ) : (↑(q ^ n) : ℚ) = q ^ n := coe_hom.map_pow _ _
-
-@[norm_cast] lemma coe_list_sum (l : list ℚ≥0) : (l.sum : ℚ) = (l.map coe).sum :=
-coe_hom.map_list_sum _
-
-@[norm_cast] lemma coe_list_prod (l : list ℚ≥0) : (l.prod : ℚ) = (l.map coe).prod :=
-coe_hom.map_list_prod _
-
-@[norm_cast] lemma coe_multiset_sum (s : multiset ℚ≥0) : (s.sum : ℚ) = (s.map coe).sum :=
-coe_hom.map_multiset_sum _
-
-@[norm_cast] lemma coe_multiset_prod (s : multiset ℚ≥0) : (s.prod : ℚ) = (s.map coe).prod :=
-coe_hom.map_multiset_prod _
-
-@[norm_cast] lemma coe_sum {s : finset α} {f : α → ℚ≥0} : ↑(∑ a in s, f a) = ∑ a in s, (f a : ℚ) :=
-coe_hom.map_sum _ _
-
-lemma to_nnrat_sum_of_nonneg {s : finset α} {f : α → ℚ} (hf : ∀ a, a ∈ s → 0 ≤ f a) :
-  (∑ a in s, f a).to_nnrat = ∑ a in s, (f a).to_nnrat :=
-begin
-  rw [←coe_inj, coe_sum, rat.coe_to_nnrat _ (finset.sum_nonneg hf)],
-  exact finset.sum_congr rfl (λ x hxs, by rw rat.coe_to_nnrat _ (hf x hxs)),
-end
-
-@[norm_cast] lemma coe_prod {s : finset α} {f : α → ℚ≥0} : ↑(∏ a in s, f a) = ∏ a in s, (f a : ℚ) :=
-coe_hom.map_prod _ _
-
-lemma to_nnrat_prod_of_nonneg {s : finset α} {f : α → ℚ} (hf : ∀ a ∈ s, 0 ≤ f a) :
-  (∏ a in s, f a).to_nnrat = ∏ a in s, (f a).to_nnrat :=
-begin
-  rw [←coe_inj, coe_prod, rat.coe_to_nnrat _ (finset.prod_nonneg hf)],
-  exact finset.prod_congr rfl (λ x hxs, by rw rat.coe_to_nnrat _ (hf x hxs)),
-end
-
-@[norm_cast] lemma nsmul_coe (q : ℚ≥0) (n : ℕ) : ↑(n • q) = n • (q : ℚ) :=
-coe_hom.to_add_monoid_hom.map_nsmul _ _
-
 lemma bdd_above_coe {s : set ℚ≥0} : bdd_above (coe '' s : set ℚ) ↔ bdd_above s :=
 ⟨λ ⟨b, hb⟩, ⟨to_nnrat b, λ ⟨y, hy⟩ hys, show y ≤ max b 0, from
     (hb $ set.mem_image_of_mem _ hys).trans $ le_max_left _ _⟩,
@@ -246,20 +187,6 @@ begin
     rw [to_nnrat_eq_zero.2 hq, to_nnrat_eq_zero.2 hpq, mul_zero] }
 end
 
-lemma to_nnrat_inv (q : ℚ) : to_nnrat q⁻¹ = (to_nnrat q)⁻¹ :=
-begin
-  obtain hq | hq := le_total q 0,
-  { rw [to_nnrat_eq_zero.mpr hq, inv_zero, to_nnrat_eq_zero.mpr (inv_nonpos.mpr hq)] },
-  { nth_rewrite 0 ←rat.coe_to_nnrat q hq,
-    rw [←coe_inv, to_nnrat_coe] }
-end
-
-lemma to_nnrat_div (hp : 0 ≤ p) : to_nnrat (p / q) = to_nnrat p / to_nnrat q :=
-by rw [div_eq_mul_inv, div_eq_mul_inv, ←to_nnrat_inv, ←to_nnrat_mul hp]
-
-lemma to_nnrat_div' (hq : 0 ≤ q) : to_nnrat (p / q) = to_nnrat p / to_nnrat q :=
-by rw [div_eq_inv_mul, div_eq_inv_mul, to_nnrat_mul (inv_nonneg.2 hq), to_nnrat_inv]
-
 end rat
 
 /-- The absolute value on `ℚ` as a map to `ℚ≥0`. -/
@@ -288,16 +215,4 @@ ext $ rat.ext ((int.nat_abs_inj_of_nonneg_of_nonneg
 lemma ext_num_denom_iff : p = q ↔ p.num = q.num ∧ p.denom = q.denom :=
 ⟨by { rintro rfl, exact ⟨rfl, rfl⟩ }, λ h, ext_num_denom h.1 h.2⟩
 
-@[simp] lemma num_div_denom (q : ℚ≥0) : (q.num : ℚ≥0) / q.denom = q :=
-begin
-  ext1,
-  rw [coe_div, coe_nat_cast, coe_nat_cast, num, ←int.cast_coe_nat,
-    int.nat_abs_of_nonneg (rat.num_nonneg_iff_zero_le.2 q.prop)],
-  exact rat.num_div_denom q,
-end
-
-/-- A recursor for nonnegative rationals in terms of numerators and denominators. -/
-protected def rec {α : ℚ≥0 → Sort*} (h : Π m n : ℕ, α (m / n)) (q : ℚ≥0) : α q :=
-(num_div_denom _).rec (h _ _)
-
 end nnrat

src/data/rat/nnrat/lemmas.lean

@@ -0,0 +1,65 @@
+/-
+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 algebra.algebra.basic
+import algebra.indicator_function
+import data.rat.basic
+
+/-!
+# 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_locale big_operators nnrat
+
+namespace nnrat
+variables {α : Type*} {p q : ℚ≥0}
+
+/-- The rational numbers are an algebra over the non-negative rationals. -/
+instance : algebra ℚ≥0 ℚ := coe_hom.to_algebra
+
+/-- A `module` over `ℚ` restricts to a `module` over `ℚ≥0`. -/
+instance [add_comm_monoid α] [module ℚ α] : module ℚ≥0 α := module.comp_hom α coe_hom
+
+@[simp, norm_cast] lemma coe_indicator (s : set α) (f : α → ℚ≥0) (a : α) :
+  ((s.indicator f a : ℚ≥0) : ℚ) = s.indicator (λ x, f x) a :=
+(coe_hom : ℚ≥0 →+ ℚ).map_indicator _ _ _
+
+@[norm_cast] lemma coe_list_sum (l : list ℚ≥0) : (l.sum : ℚ) = (l.map coe).sum :=
+coe_hom.map_list_sum _
+
+@[norm_cast] lemma coe_list_prod (l : list ℚ≥0) : (l.prod : ℚ) = (l.map coe).prod :=
+coe_hom.map_list_prod _
+
+@[norm_cast] lemma coe_multiset_sum (s : multiset ℚ≥0) : (s.sum : ℚ) = (s.map coe).sum :=
+coe_hom.map_multiset_sum _
+
+@[norm_cast] lemma coe_multiset_prod (s : multiset ℚ≥0) : (s.prod : ℚ) = (s.map coe).prod :=
+coe_hom.map_multiset_prod _
+
+@[norm_cast] lemma coe_sum {s : finset α} {f : α → ℚ≥0} : ↑(∑ a in s, f a) = ∑ a in s, (f a : ℚ) :=
+coe_hom.map_sum _ _
+
+lemma to_nnrat_sum_of_nonneg {s : finset α} {f : α → ℚ} (hf : ∀ a, a ∈ s → 0 ≤ f a) :
+  (∑ a in s, f a).to_nnrat = ∑ a in s, (f a).to_nnrat :=
+begin
+  rw [←coe_inj, coe_sum, rat.coe_to_nnrat _ (finset.sum_nonneg hf)],
+  exact finset.sum_congr rfl (λ x hxs, by rw rat.coe_to_nnrat _ (hf x hxs)),
+end
+
+@[norm_cast] lemma coe_prod {s : finset α} {f : α → ℚ≥0} : ↑(∏ a in s, f a) = ∏ a in s, (f a : ℚ) :=
+coe_hom.map_prod _ _
+
+lemma to_nnrat_prod_of_nonneg {s : finset α} {f : α → ℚ} (hf : ∀ a ∈ s, 0 ≤ f a) :
+  (∏ a in s, f a).to_nnrat = ∏ a in s, (f a).to_nnrat :=
+begin
+  rw [←coe_inj, coe_prod, rat.coe_to_nnrat _ (finset.prod_nonneg hf)],
+  exact finset.prod_congr rfl (λ x hxs, by rw rat.coe_to_nnrat _ (hf x hxs)),
+end
+
+end nnrat

src/data/rat/order.lean

@@ -3,9 +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 algebra.order.field.defs
-import data.rat.basic
 import data.int.cast.lemmas
+import data.rat.defs
 import tactic.assert_exists
 
 /-!
@@ -14,18 +13,21 @@ import tactic.assert_exists
 > THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
 > Any changes to this file require a corresponding PR to mathlib4.
 
-## Summary
+We define the order on `ℚ`, prove that `ℚ` is a discrete, linearly ordered ring, and define
+functions such as `abs` that depend on this order.
 
-We define the order on `ℚ`, prove that `ℚ` is a discrete, linearly ordered field, and define
-functions such as `abs` and `sqrt` that depend on this order.
+## Notes
+
+The `linear_ordered_field` instance is to be found in `data.rat.basic` because putting it here would
+result in import cycles.
 
 ## Notations
 
 - `/.` is infix notation for `rat.mk`.
 
 ## Tags
 
-rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering, sqrt, abs
+rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering, abs
 -/
 
 namespace rat
@@ -163,18 +165,16 @@ by unfold has_le.le rat.le; rw add_sub_add_left_eq_sub
 protected theorem mul_nonneg {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b :=
 by rw ← nonneg_iff_zero_le at ha hb ⊢; exact rat.nonneg_mul ha hb
 
-instance : linear_ordered_field ℚ :=
+instance : linear_ordered_comm_ring ℚ :=
 { zero_le_one     := dec_trivial,
+  exists_pair_ne  := ⟨0, 1, dec_trivial⟩,
   add_le_add_left := assume a b ab c, rat.add_le_add_left.2 ab,
   mul_pos         := assume 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,
-  ..rat.field,
-  ..rat.linear_order,
-  ..rat.semiring }
+  ..rat.comm_ring, ..rat.linear_order }
 
 /- Extra instances to short-circuit type class resolution -/
-instance : linear_ordered_comm_ring ℚ       := by apply_instance
 instance : linear_ordered_ring ℚ            := by apply_instance
 instance : ordered_ring ℚ                   := by apply_instance
 instance : linear_ordered_semiring ℚ        := by apply_instance