From 46361cfe5479635f8c1a2f67f7523e178957ec8f Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 5 Jun 2024 23:56:03 +0000
Subject: [PATCH 01/17] feat: add lemmas for NNRat

---
 Mathlib/Data/NNRat/Defs.lean     |  6 +++++
 Mathlib/Data/Rat/Cast/Order.lean | 39 ++++++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+)

diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
index dea427072ed7f..34371755e2a9e 100644
--- a/Mathlib/Data/NNRat/Defs.lean
+++ b/Mathlib/Data/NNRat/Defs.lean
@@ -440,4 +440,10 @@ lemma add_def (q r : ℚ≥0) : q + r = divNat (q.num * r.den + r.num * q.den) (
 lemma mul_def (q r : ℚ≥0) : q * r = divNat (q.num * r.num) (q.den * r.den) := by
   ext; simp [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, num_coe, den_coe]
 
+theorem lt_def {p q : ℚ≥0} : p < q ↔ p.num * q.den < q.num * p.den := by
+  rw [← NNRat.coe_lt_coe, Rat.lt_def]; norm_cast
+
+theorem le_def {p q : ℚ≥0} : p ≤ q ↔ p.num * q.den ≤ q.num * p.den := by
+  rw [← NNRat.coe_le_coe, Rat.le_def]; norm_cast
+
 end NNRat
diff --git a/Mathlib/Data/Rat/Cast/Order.lean b/Mathlib/Data/Rat/Cast/Order.lean
index fd0ec2366fc04..a0add505126e6 100644
--- a/Mathlib/Data/Rat/Cast/Order.lean
+++ b/Mathlib/Data/Rat/Cast/Order.lean
@@ -148,6 +148,45 @@ theorem preimage_cast_uIoc (a b : ℚ) : (↑) ⁻¹' uIoc (a : K) b = uIoc a b
 end LinearOrderedField
 end Rat
 
+namespace NNRat
+
+variable {K} [LinearOrderedSemifield K]
+
+theorem cast_strictMono : StrictMono ((↑) : ℚ≥0 → K) := fun m n h => by
+  rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_lt,
+    ← NNRat.lt_def]
+  -- · norm_num
+  -- · norm_num
+
+/-- Coercion from `ℚ` as an order embedding. -/
+@[simps!]
+def castOrderEmbedding : ℚ≥0 ↪o K :=
+  OrderEmbedding.ofStrictMono (↑) cast_strictMono
+
+@[simp, norm_cast]
+theorem cast_le {m n : ℚ≥0} : (m : K) ≤ n ↔ m ≤ n :=
+  castOrderEmbedding.le_iff_le
+
+@[simp, norm_cast]
+theorem cast_lt {m n : ℚ≥0} : (m : K) < n ↔ m < n :=
+  cast_strictMono.lt_iff_lt
+
+@[simp]
+theorem cast_pos {n : ℚ≥0} : (0 : K) < n ↔ 0 < n := by
+  norm_cast
+
+@[simp, norm_cast]
+theorem cast_min {a b : ℚ} : (↑(min a b) : K) = min (a : K) (b : K) :=
+  (@cast_mono K _).map_min
+#align rat.cast_min Rat.cast_min
+
+@[simp, norm_cast]
+theorem cast_max {a b : ℚ} : (↑(max a b) : K) = max (a : K) (b : K) :=
+  (@cast_mono K _).map_max
+#align rat.cast_max Rat.cast_max
+
+end NNRat
+
 namespace Mathlib.Meta.Positivity
 open Lean Meta Qq Function
 

From 987cddc2b3dd1ed26e33ddfe44c55cdf58b9caea Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Jun 2024 00:11:07 +0000
Subject: [PATCH 02/17] more

---
 Mathlib/Data/Rat/Cast/Order.lean | 84 +++++++++++++++++++++++++++++---
 1 file changed, 76 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Rat/Cast/Order.lean b/Mathlib/Data/Rat/Cast/Order.lean
index a0add505126e6..7a7bb97fa2858 100644
--- a/Mathlib/Data/Rat/Cast/Order.lean
+++ b/Mathlib/Data/Rat/Cast/Order.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import Mathlib.Algebra.Order.Ring.Rat
 import Mathlib.Data.Rat.Cast.CharZero
 import Mathlib.Tactic.Positivity.Core
+import Mathlib.Algebra.Order.Field.Basic
 
 #align_import data.rat.cast from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
 
@@ -153,10 +154,14 @@ namespace NNRat
 variable {K} [LinearOrderedSemifield K]
 
 theorem cast_strictMono : StrictMono ((↑) : ℚ≥0 → K) := fun m n h => by
-  rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_lt,
-    ← NNRat.lt_def]
-  -- · norm_num
-  -- · norm_num
+  rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff, ← Nat.cast_mul, ← Nat.cast_mul,
+    Nat.cast_lt (α := K), ← NNRat.lt_def]
+  · simp
+  · simp
+
+@[mono]
+theorem cast_mono : Monotone ((↑) : ℚ≥0 → K) :=
+  cast_strictMono.monotone
 
 /-- Coercion from `ℚ` as an order embedding. -/
 @[simps!]
@@ -171,19 +176,68 @@ theorem cast_le {m n : ℚ≥0} : (m : K) ≤ n ↔ m ≤ n :=
 theorem cast_lt {m n : ℚ≥0} : (m : K) < n ↔ m < n :=
   cast_strictMono.lt_iff_lt
 
+
+@[simp]
+theorem cast_nonpos {n : ℚ≥0} : (n : K) ≤ 0 ↔ n ≤ 0 := by
+  norm_cast
+
 @[simp]
 theorem cast_pos {n : ℚ≥0} : (0 : K) < n ↔ 0 < n := by
   norm_cast
 
+@[simp]
+theorem cast_lt_zero {n : ℚ≥0} : (n : K) < 0 ↔ n < 0 := by
+  norm_cast
+
 @[simp, norm_cast]
-theorem cast_min {a b : ℚ} : (↑(min a b) : K) = min (a : K) (b : K) :=
+theorem cast_min {a b : ℚ≥0} : (↑(min a b) : K) = min (a : K) (b : K) :=
   (@cast_mono K _).map_min
-#align rat.cast_min Rat.cast_min
 
 @[simp, norm_cast]
-theorem cast_max {a b : ℚ} : (↑(max a b) : K) = max (a : K) (b : K) :=
+theorem cast_max {a b : ℚ≥0} : (↑(max a b) : K) = max (a : K) (b : K) :=
   (@cast_mono K _).map_max
-#align rat.cast_max Rat.cast_max
+
+open Set
+
+@[simp]
+theorem preimage_cast_Icc (a b : ℚ≥0) : (↑) ⁻¹' Icc (a : K) b = Icc a b :=
+  castOrderEmbedding.preimage_Icc ..
+
+@[simp]
+theorem preimage_cast_Ico (a b : ℚ≥0) : (↑) ⁻¹' Ico (a : K) b = Ico a b :=
+  castOrderEmbedding.preimage_Ico ..
+
+@[simp]
+theorem preimage_cast_Ioc (a b : ℚ≥0) : (↑) ⁻¹' Ioc (a : K) b = Ioc a b :=
+  castOrderEmbedding.preimage_Ioc a b
+
+@[simp]
+theorem preimage_cast_Ioo (a b : ℚ≥0) : (↑) ⁻¹' Ioo (a : K) b = Ioo a b :=
+  castOrderEmbedding.preimage_Ioo a b
+
+@[simp]
+theorem preimage_cast_Ici (a : ℚ≥0) : (↑) ⁻¹' Ici (a : K) = Ici a :=
+  castOrderEmbedding.preimage_Ici a
+
+@[simp]
+theorem preimage_cast_Iic (a : ℚ≥0) : (↑) ⁻¹' Iic (a : K) = Iic a :=
+  castOrderEmbedding.preimage_Iic a
+
+@[simp]
+theorem preimage_cast_Ioi (a : ℚ≥0) : (↑) ⁻¹' Ioi (a : K) = Ioi a :=
+  castOrderEmbedding.preimage_Ioi a
+
+@[simp]
+theorem preimage_cast_Iio (a : ℚ≥0) : (↑) ⁻¹' Iio (a : K) = Iio a :=
+  castOrderEmbedding.preimage_Iio a
+
+@[simp]
+theorem preimage_cast_uIcc (a b : ℚ≥0) : (↑) ⁻¹' uIcc (a : K) b = uIcc a b :=
+  (castOrderEmbedding (K := K)).preimage_uIcc a b
+
+@[simp]
+theorem preimage_cast_uIoc (a b : ℚ≥0) : (↑) ⁻¹' uIoc (a : K) b = uIoc a b :=
+  (castOrderEmbedding (K := K)).preimage_uIoc a b
 
 end NNRat
 
@@ -210,4 +264,18 @@ def evalRatCast : PositivityExt where eval {u α} _zα _pα e := do
     return .nonzero q((Rat.cast_ne_zero (α := $α)).mpr $pa)
   | .none => pure .none
 
+/-- Extension for NNRat.cast. -/
+@[positivity NNRat.cast _]
+def evalNNRatCast : PositivityExt where eval {u α} _zα _pα e := do
+  let ~q(@NNRat.cast _ (_) ($a : ℚ≥0)) := e | throwError "not NNRat.cast"
+  match ← core q(inferInstance) q(inferInstance) a with
+  | .positive pa =>
+    let _oα ← synthInstanceQ q(LinearOrderedSemifield $α)
+    assumeInstancesCommute
+    return .positive q((NNRat.cast_pos (K := $α)).mpr $pa)
+  | _ =>
+    let _oα ← synthInstanceQ q(LinearOrderedSemifield $α)
+    assumeInstancesCommute
+    return .nonnegative q(NNRat.cast_nonneg _)
+
 end Mathlib.Meta.Positivity

From 1d468be43b552d65bf758a874f954bbc94917952 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Jun 2024 00:12:28 +0000
Subject: [PATCH 03/17] whitespace

---
 Mathlib/Data/Rat/Cast/Order.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Rat/Cast/Order.lean b/Mathlib/Data/Rat/Cast/Order.lean
index 7a7bb97fa2858..199b5c2def00b 100644
--- a/Mathlib/Data/Rat/Cast/Order.lean
+++ b/Mathlib/Data/Rat/Cast/Order.lean
@@ -176,7 +176,6 @@ theorem cast_le {m n : ℚ≥0} : (m : K) ≤ n ↔ m ≤ n :=
 theorem cast_lt {m n : ℚ≥0} : (m : K) < n ↔ m < n :=
   cast_strictMono.lt_iff_lt
 
-
 @[simp]
 theorem cast_nonpos {n : ℚ≥0} : (n : K) ≤ 0 ↔ n ≤ 0 := by
   norm_cast

From d00d9442757935d47136d657cbe04306c596afa9 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Jun 2024 00:13:21 +0000
Subject: [PATCH 04/17] feat: add a FloorSemiring instance to nnrat

---
 Mathlib/Data/NNRat/Floor.lean | 80 +++++++++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)
 create mode 100644 Mathlib/Data/NNRat/Floor.lean

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
new file mode 100644
index 0000000000000..eca395cc4768c
--- /dev/null
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2019 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Data.Rat.Floor
+import Mathlib.Data.NNRat.Lemmas
+
+/-!
+# Floor Function for Non-negative Rational Numbers
+
+## Summary
+
+We define the `FloorRing` instance on `ℚ≥0`. Some technical lemmas relating `floor` to integer
+division and modulo arithmetic are derived as well as some simple inequalities.
+
+## Tags
+
+nnrat, rationals, ℚ≥0, floor
+-/
+
+namespace NNRat
+
+instance : FloorSemiring ℚ≥0 where
+  floor q := ⌊q.val⌋₊
+  ceil q := ⌈q.val⌉₊
+  floor_of_neg h := by simpa using h.trans zero_lt_one
+  gc_floor {a n} h := by rw [← NNRat.coe_le_coe, Nat.le_floor_iff] <;> norm_cast
+  gc_ceil {a b} := by rw [← NNRat.coe_le_coe, Nat.ceil_le]; norm_cast
+
+theorem floor_coe (q : ℚ≥0) : ⌊(q : ℚ)⌋₊ = ⌊q⌋₊ := rfl
+
+theorem ceil_coe (q : ℚ≥0) : ⌈(q : ℚ)⌉₊ = ⌈q⌉₊ := rfl
+
+@[simp, norm_cast]
+theorem coe_floor (q : ℚ≥0) : ↑⌊q⌋₊ = ⌊(q : ℚ)⌋ := Int.ofNat_floor_eq_floor q.coe_nonneg
+
+@[simp, norm_cast]
+theorem coe_ceil (q : ℚ≥0) : ↑⌈q⌉₊ = ⌈(q : ℚ)⌉ := Int.ofNat_ceil_eq_ceil q.coe_nonneg
+
+protected theorem floor_def (q : ℚ≥0) : ⌊q⌋₊ = q.num / q.den := by
+  rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def, Int.ofNat_ediv, den_coe, num_coe]
+
+
+variables {K} [LinearOrderedSemifield K] [FloorSemiring K]
+#check Rat.cast_mono
+theorem cast_strictMono : StrictMono ((↑) : ℚ≥0 → K) := fun m n h => by
+  rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_lt,
+    ← NNRat.lt_def]
+  · norm_num
+  · norm_num
+
+/-- Coercion from `ℚ` as an order embedding. -/
+@[simps!]
+def castOrderEmbedding : ℚ≥0 ↪o K :=
+  OrderEmbedding.ofStrictMono (↑) cast_strictMono
+
+@[simp, norm_cast]
+theorem cast_le {m n : ℚ≥0} : (m : K) ≤ n ↔ m ≤ n :=
+  castOrderEmbedding.le_iff_le
+
+@[simp, norm_cast]
+theorem cast_lt {m n : ℚ≥0} : (m : K) < n ↔ m < n :=
+  cast_strictMono.lt_iff_lt
+
+@[simp, norm_cast]
+theorem floor_cast (x : ℚ≥0) : ⌊(x : K)⌋₊ = ⌊x⌋₊ := by
+  have := (Nat.floor_eq_iff x.cast_nonneg).1 (Eq.refl ⌊x⌋₊)
+  refine (Nat.floor_eq_iff x.cast_nonneg).2 ?_
+  rw [← NNRat.cast_lt (K := K)] at this
+  rw [← NNRat.cast_natCast, NNRat.cast_le] at this ⊢
+  convert this
+#align rat.floor_cast Rat.floor_cast
+
+@[simp, norm_cast]
+theorem ceil_cast (x : ℚ≥0) : ⌈(x : K)⌉₊ = ⌈x⌉₊ := by
+  rw [Nat.ceil_eq_iff]
+  rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
+#align rat.ceil_cast Rat.ceil_cast
+end NNRat

From e4a084ec239fbe538df3dacd3fb5b4aa310cc537 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Jun 2024 00:14:41 +0000
Subject: [PATCH 05/17] fix

---
 Mathlib/Data/NNRat/Floor.lean | 22 ----------------------
 1 file changed, 22 deletions(-)

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index eca395cc4768c..c801c98660209 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -41,28 +41,6 @@ theorem coe_ceil (q : ℚ≥0) : ↑⌈q⌉₊ = ⌈(q : ℚ)⌉ := Int.ofNat_ce
 protected theorem floor_def (q : ℚ≥0) : ⌊q⌋₊ = q.num / q.den := by
   rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def, Int.ofNat_ediv, den_coe, num_coe]
 
-
-variables {K} [LinearOrderedSemifield K] [FloorSemiring K]
-#check Rat.cast_mono
-theorem cast_strictMono : StrictMono ((↑) : ℚ≥0 → K) := fun m n h => by
-  rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_lt,
-    ← NNRat.lt_def]
-  · norm_num
-  · norm_num
-
-/-- Coercion from `ℚ` as an order embedding. -/
-@[simps!]
-def castOrderEmbedding : ℚ≥0 ↪o K :=
-  OrderEmbedding.ofStrictMono (↑) cast_strictMono
-
-@[simp, norm_cast]
-theorem cast_le {m n : ℚ≥0} : (m : K) ≤ n ↔ m ≤ n :=
-  castOrderEmbedding.le_iff_le
-
-@[simp, norm_cast]
-theorem cast_lt {m n : ℚ≥0} : (m : K) < n ↔ m < n :=
-  cast_strictMono.lt_iff_lt
-
 @[simp, norm_cast]
 theorem floor_cast (x : ℚ≥0) : ⌊(x : K)⌋₊ = ⌊x⌋₊ := by
   have := (Nat.floor_eq_iff x.cast_nonneg).1 (Eq.refl ⌊x⌋₊)

From 41f1de7e7c9b0bff3a7f3320f67e944d20a3ef35 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Jun 2024 00:16:00 +0000
Subject: [PATCH 06/17] whitespace

---
 Mathlib/Data/NNRat/Floor.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index c801c98660209..c0896b3cd8bad 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -55,4 +55,5 @@ theorem ceil_cast (x : ℚ≥0) : ⌈(x : K)⌉₊ = ⌈x⌉₊ := by
   rw [Nat.ceil_eq_iff]
   rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
 #align rat.ceil_cast Rat.ceil_cast
+
 end NNRat

From 422a5d53e772543d24f1c804e8c028760cd8a34d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 9 Jun 2024 09:24:29 +0000
Subject: [PATCH 07/17] working

---
 Mathlib/Data/NNRat/Floor.lean    | 22 +++++++--------
 Mathlib/Data/Rat/Cast/Order.lean | 48 ++++++++++++++++++++++++++++++++
 2 files changed, 58 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index c0896b3cd8bad..d570e4611e73a 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -11,8 +11,9 @@ import Mathlib.Data.NNRat.Lemmas
 
 ## Summary
 
-We define the `FloorRing` instance on `ℚ≥0`. Some technical lemmas relating `floor` to integer
-division and modulo arithmetic are derived as well as some simple inequalities.
+We define the `FloorSemiring` instance on `ℚ≥0`, and relate it's operators to `NNRat.cast`.
+
+Note that we cannot talk about `Int.fract`, which currently only works for rings.
 
 ## Tags
 
@@ -41,19 +42,16 @@ theorem coe_ceil (q : ℚ≥0) : ↑⌈q⌉₊ = ⌈(q : ℚ)⌉ := Int.ofNat_ce
 protected theorem floor_def (q : ℚ≥0) : ⌊q⌋₊ = q.num / q.den := by
   rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def, Int.ofNat_ediv, den_coe, num_coe]
 
+variable {K} [LinearOrderedSemifield K] [FloorSemiring K]
+
 @[simp, norm_cast]
-theorem floor_cast (x : ℚ≥0) : ⌊(x : K)⌋₊ = ⌊x⌋₊ := by
-  have := (Nat.floor_eq_iff x.cast_nonneg).1 (Eq.refl ⌊x⌋₊)
-  refine (Nat.floor_eq_iff x.cast_nonneg).2 ?_
-  rw [← NNRat.cast_lt (K := K)] at this
-  rw [← NNRat.cast_natCast, NNRat.cast_le] at this ⊢
-  convert this
-#align rat.floor_cast Rat.floor_cast
+theorem floor_cast (x : ℚ≥0) : ⌊(x : K)⌋₊ = ⌊x⌋₊ :=
+  (Nat.floor_eq_iff x.cast_nonneg).2 (mod_cast (Nat.floor_eq_iff x.cast_nonneg).1 (Eq.refl ⌊x⌋₊))
 
 @[simp, norm_cast]
 theorem ceil_cast (x : ℚ≥0) : ⌈(x : K)⌉₊ = ⌈x⌉₊ := by
-  rw [Nat.ceil_eq_iff]
-  rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
-#align rat.ceil_cast Rat.ceil_cast
+  obtain rfl | hx := eq_or_ne x 0
+  · simp
+  · refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊)) <;> simpa
 
 end NNRat
diff --git a/Mathlib/Data/Rat/Cast/Order.lean b/Mathlib/Data/Rat/Cast/Order.lean
index fec5653e6cfc6..3ea29974b0d52 100644
--- a/Mathlib/Data/Rat/Cast/Order.lean
+++ b/Mathlib/Data/Rat/Cast/Order.lean
@@ -81,6 +81,38 @@ theorem cast_lt_zero {n : ℚ} : (n : K) < 0 ↔ n < 0 := by
   norm_cast
 #align rat.cast_lt_zero Rat.cast_lt_zero
 
+@[simp, norm_cast]
+theorem cast_le_natCast {m : ℚ} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ) := by
+  rw [← cast_le (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem natCast_le_cast {m : ℕ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n := by
+  rw [← cast_le (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem cast_le_intCast {m : ℚ} {n : ℤ} : (m : K) ≤ n ↔ m ≤ (n : ℚ) := by
+  rw [← cast_le (K := K), cast_intCast]
+
+@[simp, norm_cast]
+theorem intCast_le_cast {m : ℤ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n := by
+  rw [← cast_le (K := K), cast_intCast]
+
+@[simp, norm_cast]
+theorem cast_lt_natCast {m : ℚ} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ) := by
+  rw [← cast_lt (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem natCast_lt_cast {m : ℕ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n := by
+  rw [← cast_lt (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem cast_lt_intCast {m : ℚ} {n : ℤ} : (m : K) < n ↔ m < (n : ℚ) := by
+  rw [← cast_lt (K := K), cast_intCast]
+
+@[simp, norm_cast]
+theorem intCast_lt_cast {m : ℤ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n := by
+  rw [← cast_lt (K := K), cast_intCast]
+
 @[simp, norm_cast]
 theorem cast_min {a b : ℚ} : (↑(min a b) : K) = min (a : K) (b : K) :=
   (@cast_mono K _).map_min
@@ -191,6 +223,22 @@ theorem cast_lt_zero {n : ℚ≥0} : (n : K) < 0 ↔ n < 0 := by
 @[simp]
 theorem not_cast_lt_zero {n : ℚ≥0} : ¬(n : K) < 0 := mod_cast not_lt_zero'
 
+@[simp, norm_cast]
+theorem cast_le_natCast {m : ℚ≥0} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ≥0) := by
+  rw [← cast_le (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem natCast_le_cast {m : ℕ} {n : ℚ≥0} : (m : K) ≤ n ↔ (m : ℚ≥0) ≤ n := by
+  rw [← cast_le (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem cast_lt_natCast {m : ℚ≥0} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ≥0) := by
+  rw [← cast_lt (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem natCast_lt_cast {m : ℕ} {n : ℚ≥0} : (m : K) < n ↔ (m : ℚ≥0) < n := by
+  rw [← cast_lt (K := K), cast_natCast]
+
 @[simp, norm_cast]
 theorem cast_min {a b : ℚ≥0} : (↑(min a b) : K) = min (a : K) (b : K) :=
   (@cast_mono K _).map_min

From 8c3eb6e930751613728811853f69833ecce0165f Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 22 Jul 2024 23:36:25 +0100
Subject: [PATCH 08/17] Update Floor.lean

---
 Mathlib/Data/NNRat/Floor.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index d570e4611e73a..c7e7dba96f285 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2019 Eric Wieser. All rights reserved.
+Copyright (c) 2024 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/

From 900b41fc401c56c85ad532d04e32f207b4b98e1b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 22 Jul 2024 22:40:38 +0000
Subject: [PATCH 09/17] add import

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index ecfcda062137d..e05ebca42168f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2252,6 +2252,7 @@ import Mathlib.Data.Multiset.Sum
 import Mathlib.Data.Multiset.Sym
 import Mathlib.Data.NNRat.BigOperators
 import Mathlib.Data.NNRat.Defs
+import Mathlib.Data.NNRat.Floor
 import Mathlib.Data.NNRat.Lemmas
 import Mathlib.Data.NNReal.Basic
 import Mathlib.Data.NNReal.Star

From 8e1768ddac675f2026fee5454fb74f1d53ad05ed Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 22 Jul 2024 23:05:29 +0000
Subject: [PATCH 10/17] add lemmas

---
 Mathlib/Data/NNRat/Defs.lean  |  3 +++
 Mathlib/Data/NNRat/Floor.lean |  4 ++++
 Mathlib/Data/Rat/Floor.lean   | 17 +++++++++++++++--
 3 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
index c95a6d273e5f4..a74cdf27bbe3b 100644
--- a/Mathlib/Data/NNRat/Defs.lean
+++ b/Mathlib/Data/NNRat/Defs.lean
@@ -92,6 +92,9 @@ theorem coe_nonneg (q : ℚ≥0) : (0 : ℚ) ≤ q :=
 
 @[simp, norm_cast] lemma coe_one : ((1 : ℚ≥0) : ℚ) = 1 := rfl
 
+@[simp] lemma num_zero : num 0 = 0 := rfl
+@[simp] lemma den_zero : den 0 = 1 := rfl
+
 @[simp, norm_cast]
 theorem coe_add (p q : ℚ≥0) : ((p + q : ℚ≥0) : ℚ) = p + q :=
   rfl
diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index c7e7dba96f285..c12d2d605a892 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -54,4 +54,8 @@ theorem ceil_cast (x : ℚ≥0) : ⌈(x : K)⌉₊ = ⌈x⌉₊ := by
   · simp
   · refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊)) <;> simpa
 
+@[norm_cast]
+theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ≥0)⌋₊ = n / d :=
+  Rat.natFloor_natCast_div_natCast n d
+
 end NNRat
diff --git a/Mathlib/Data/Rat/Floor.lean b/Mathlib/Data/Rat/Floor.lean
index 7e7f210c19ae8..f893856fbbe01 100644
--- a/Mathlib/Data/Rat/Floor.lean
+++ b/Mathlib/Data/Rat/Floor.lean
@@ -49,7 +49,8 @@ instance : FloorRing ℚ :=
 
 protected theorem floor_def {q : ℚ} : ⌊q⌋ = q.num / q.den := Rat.floor_def' q
 
-theorem floor_int_div_nat_eq_div {n : ℤ} {d : ℕ} : ⌊(↑n : ℚ) / (↑d : ℚ)⌋ = n / (↑d : ℤ) := by
+@[norm_cast]
+theorem floor_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / (↑d : ℤ) := by
   rw [Rat.floor_def]
   obtain rfl | hd := @eq_zero_or_pos _ _ d
   · simp
@@ -61,6 +62,18 @@ theorem floor_int_div_nat_eq_div {n : ℤ} {d : ℕ} : ⌊(↑n : ℚ) / (↑d :
   refine (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left ?_ <| Int.natCast_nonneg q.den).symm
   rwa [← d_eq_c_mul_denom, Int.natCast_pos]
 
+@[norm_cast]
+theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / d :=
+  floor_intCast_div_natCast n d
+
+@[norm_cast]
+theorem natFloor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋₊ = n / d := by
+  rw [← Int.ofNat_inj, Int.ofNat_floor_eq_floor (by positivity)]
+  push_cast
+  exact floor_intCast_div_natCast n d
+
+@[deprecated (since := "2024-07-23")] alias floor_int_div_nat_eq_div := floor_intCast_div_natCast
+
 @[simp, norm_cast]
 theorem floor_cast (x : ℚ) : ⌊(x : α)⌋ = ⌊x⌋ :=
   floor_eq_iff.2 (mod_cast floor_eq_iff.1 (Eq.refl ⌊x⌋))
@@ -81,7 +94,7 @@ theorem cast_fract (x : ℚ) : (↑(fract x) : α) = fract (x : α) := by
 end Rat
 
 theorem Int.mod_nat_eq_sub_mul_floor_rat_div {n : ℤ} {d : ℕ} : n % d = n - d * ⌊(n : ℚ) / d⌋ := by
-  rw [eq_sub_of_add_eq <| Int.emod_add_ediv n d, Rat.floor_int_div_nat_eq_div]
+  rw [eq_sub_of_add_eq <| Int.emod_add_ediv n d, Rat.floor_intCast_div_natCast]
 
 theorem Nat.coprime_sub_mul_floor_rat_div_of_coprime {n d : ℕ} (n_coprime_d : n.Coprime d) :
     ((n : ℤ) - d * ⌊(n : ℚ) / d⌋).natAbs.Coprime d := by

From fbed638522c6ee16d7ae2b7319a7cbb298d981dd Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 22 Jul 2024 23:10:30 +0000
Subject: [PATCH 11/17] more silly lemmas

---
 Mathlib/Data/NNRat/Defs.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
index a74cdf27bbe3b..f0d305f2fa6e2 100644
--- a/Mathlib/Data/NNRat/Defs.lean
+++ b/Mathlib/Data/NNRat/Defs.lean
@@ -89,12 +89,13 @@ theorem coe_nonneg (q : ℚ≥0) : (0 : ℚ) ≤ q :=
   q.2
 
 @[simp, norm_cast] lemma coe_zero : ((0 : ℚ≥0) : ℚ) = 0 := rfl
-
-@[simp, norm_cast] lemma coe_one : ((1 : ℚ≥0) : ℚ) = 1 := rfl
-
 @[simp] lemma num_zero : num 0 = 0 := rfl
 @[simp] lemma den_zero : den 0 = 1 := rfl
 
+@[simp, norm_cast] lemma coe_one : ((1 : ℚ≥0) : ℚ) = 1 := rfl
+@[simp] lemma num_one : num 1 = 1 := rfl
+@[simp] lemma den_one : den 1 = 1 := rfl
+
 @[simp, norm_cast]
 theorem coe_add (p q : ℚ≥0) : ((p + q : ℚ≥0) : ℚ) = p + q :=
   rfl

From 0c0206fc386ecfe203ceea66c078ec4c7dfab3b3 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 23 Jul 2024 08:48:01 +0000
Subject: [PATCH 12/17] shake

---
 Mathlib/Data/NNRat/Floor.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index c12d2d605a892..0ecf1694ba7e0 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Data.Rat.Floor
-import Mathlib.Data.NNRat.Lemmas
 
 /-!
 # Floor Function for Non-negative Rational Numbers

From 97859f6691f582a4d8ebfe5ca0e11ec23585d46a Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 5 Aug 2024 21:35:44 +0000
Subject: [PATCH 13/17] grammar fix

---
 Mathlib/Data/NNRat/Floor.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index 0ecf1694ba7e0..96e664f7bdf65 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -10,7 +10,7 @@ import Mathlib.Data.Rat.Floor
 
 ## Summary
 
-We define the `FloorSemiring` instance on `ℚ≥0`, and relate it's operators to `NNRat.cast`.
+We define the `FloorSemiring` instance on `ℚ≥0`, and relate its operators to `NNRat.cast`.
 
 Note that we cannot talk about `Int.fract`, which currently only works for rings.
 

From a5f49e80eaa79f6e6d888f3005dfbfdf52521912 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 18 Aug 2024 22:09:16 +0000
Subject: [PATCH 14/17] more lemmas

---
 Mathlib/Data/NNRat/Floor.lean | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index 96e664f7bdf65..9cfc5b0525d07 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -41,6 +41,8 @@ theorem coe_ceil (q : ℚ≥0) : ↑⌈q⌉₊ = ⌈(q : ℚ)⌉ := Int.ofNat_ce
 protected theorem floor_def (q : ℚ≥0) : ⌊q⌋₊ = q.num / q.den := by
   rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def, Int.ofNat_ediv, den_coe, num_coe]
 
+section Semifield
+
 variable {K} [LinearOrderedSemifield K] [FloorSemiring K]
 
 @[simp, norm_cast]
@@ -53,6 +55,35 @@ theorem ceil_cast (x : ℚ≥0) : ⌈(x : K)⌉₊ = ⌈x⌉₊ := by
   · simp
   · refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊)) <;> simpa
 
+end Semifield
+
+section Field
+
+variable {K} [LinearOrderedField K] [FloorRing K]
+
+#check NNRat.natCast_le_cast
+
+@[simp, norm_cast]
+theorem intFloor_cast (x : ℚ≥0) : ⌊(x : K)⌋ = ⌊(x : ℚ)⌋ := by
+  rw [Int.floor_eq_iff (α := K), ← coe_floor]
+  norm_cast
+  norm_cast
+  rw [Nat.cast_add_one, ← Nat.floor_eq_iff (zero_le _)]
+
+@[simp, norm_cast]
+theorem intCeil_cast (x : ℚ≥0) : ⌈(x : K)⌉ = ⌈(x : ℚ)⌉ := by
+  obtain rfl | hx := eq_or_ne x 0
+  · simp only [cast_zero, Int.ceil_zero]
+  · rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]
+    constructor
+    · have := NNRat.cast_strictMono (K := K) <| Nat.ceil_lt_add_one <| zero_le x
+      sorry
+    · norm_cast
+      norm_cast
+      rw [← Nat.ceil_le]
+
+end Field
+
 @[norm_cast]
 theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ≥0)⌋₊ = n / d :=
   Rat.natFloor_natCast_div_natCast n d

From b7d6be9befc9dd56e0c48c719f5ab99be258ddb5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 18 Aug 2024 22:22:35 +0000
Subject: [PATCH 15/17] sorry-free

---
 Mathlib/Data/NNRat/Floor.lean | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index c73259c81f765..e37d20b66b386 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -70,15 +70,14 @@ theorem intFloor_cast (x : ℚ≥0) : ⌊(x : K)⌋ = ⌊(x : ℚ)⌋ := by
 
 @[simp, norm_cast]
 theorem intCeil_cast (x : ℚ≥0) : ⌈(x : K)⌉ = ⌈(x : ℚ)⌉ := by
-  obtain rfl | hx := eq_or_ne x 0
-  · simp only [cast_zero, Int.ceil_zero]
-  · rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]
-    constructor
-    · have := NNRat.cast_strictMono (K := K) <| Nat.ceil_lt_add_one <| zero_le x
-      sorry
-    · norm_cast
-      norm_cast
-      rw [← Nat.ceil_le]
+  rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]
+  constructor
+  · have := NNRat.cast_strictMono (K := K) <| Nat.ceil_lt_add_one <| zero_le x
+    rw [NNRat.cast_add, NNRat.cast_one] at this
+    refine Eq.trans_lt ?_ this
+    norm_cast
+  · rw [Int.cast_natCast, NNRat.cast_le_natCast]
+    exact Nat.le_ceil _
 
 end Field
 

From e30bc10e6b2578941d4a546d764a97daee5d5401 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 29 Aug 2024 22:16:06 +0000
Subject: [PATCH 16/17] fix deprecation

---
 Mathlib/Data/Rat/Floor.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Rat/Floor.lean b/Mathlib/Data/Rat/Floor.lean
index a1e05fcc8aa31..934ee07429cf7 100644
--- a/Mathlib/Data/Rat/Floor.lean
+++ b/Mathlib/Data/Rat/Floor.lean
@@ -106,7 +106,7 @@ theorem isInt_intFloor_ofIsRat (r : α) (n : ℤ) (d : ℕ) :
   rintro ⟨inv, rfl⟩
   constructor
   simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]
-  rw [← floor_int_div_nat_eq_div n d, ← floor_cast (α := α), Rat.cast_div,
+  rw [← floor_intCast_div_natCast n d, ← floor_cast (α := α), Rat.cast_div,
     cast_intCast, cast_natCast]
 
 /-- `norm_num` extension for `Int.floor` -/

From eaa6533716355a428a6965d5764d9a9016014665 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 31 Aug 2024 22:51:14 +0000
Subject: [PATCH 17/17] add @[simp]

---
 Mathlib/Data/NNRat/Floor.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean
index e37d20b66b386..b4fca2b5d0147 100644
--- a/Mathlib/Data/NNRat/Floor.lean
+++ b/Mathlib/Data/NNRat/Floor.lean
@@ -28,8 +28,10 @@ instance : FloorSemiring ℚ≥0 where
   gc_floor {a n} h := by rw [← NNRat.coe_le_coe, Nat.le_floor_iff] <;> norm_cast
   gc_ceil {a b} := by rw [← NNRat.coe_le_coe, Nat.ceil_le]; norm_cast
 
+@[simp, norm_cast]
 theorem floor_coe (q : ℚ≥0) : ⌊(q : ℚ)⌋₊ = ⌊q⌋₊ := rfl
 
+@[simp, norm_cast]
 theorem ceil_coe (q : ℚ≥0) : ⌈(q : ℚ)⌉₊ = ⌈q⌉₊ := rfl
 
 @[simp, norm_cast]