From c091a76f6e113b5ac95f51f434e89b7f5c1c1c5b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 24 Jan 2024 00:21:02 +0000
Subject: [PATCH 1/2] refactor: move `Archimedean` instances to
 `Order/Archimedean`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We already have the instances for `ℕ`, `ℤ`, and `ℚ` in this file, so adding `NNRat` doesn't feel that out of place.
---
 Mathlib/Algebra/Order/Archimedean.lean  | 9 +++++++++
 Mathlib/Algebra/Order/Nonneg/Floor.lean | 8 +-------
 Mathlib/Data/Rat/NNRat.lean             | 3 +--
 3 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Algebra/Order/Archimedean.lean b/Mathlib/Algebra/Order/Archimedean.lean
index d6dfd3195037b..1a4ba8bde7bf1 100644
--- a/Mathlib/Algebra/Order/Archimedean.lean
+++ b/Mathlib/Algebra/Order/Archimedean.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Int.LeastGreatest
 import Mathlib.Data.Rat.Floor
+import Mathlib.Data.Rat.NNRat
 
 #align_import algebra.order.archimedean from "leanprover-community/mathlib"@"6f413f3f7330b94c92a5a27488fdc74e6d483a78"
 
@@ -409,6 +410,14 @@ instance : Archimedean ℤ :=
 instance : Archimedean ℚ :=
   archimedean_iff_rat_le.2 fun q => ⟨q, by rw [Rat.cast_id]⟩
 
+instance Nonneg.archimedean [OrderedAddCommMonoid α] [Archimedean α] : Archimedean { x : α // 0 ≤ x } :=
+  ⟨fun x y hy =>
+    let ⟨n, hr⟩ := Archimedean.arch (x : α) (hy : (0 : α) < y)
+    ⟨n, show (x : α) ≤ (n • y : { x : α // 0 ≤ x }) by simp [*, -nsmul_eq_mul, nsmul_coe]⟩⟩
+#align nonneg.archimedean Nonneg.archimedean
+
+instance : Archimedean NNRat := Nonneg.archimedean
+
 /-- A linear ordered archimedean ring is a floor ring. This is not an `instance` because in some
 cases we have a computable `floor` function. -/
 noncomputable def Archimedean.floorRing (α) [LinearOrderedRing α] [Archimedean α] : FloorRing α :=
diff --git a/Mathlib/Algebra/Order/Nonneg/Floor.lean b/Mathlib/Algebra/Order/Nonneg/Floor.lean
index f8b1b7af83638..b521a31726d06 100644
--- a/Mathlib/Algebra/Order/Nonneg/Floor.lean
+++ b/Mathlib/Algebra/Order/Nonneg/Floor.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
+import Mathlib.Algebra.Order.Floor
 import Mathlib.Algebra.Order.Nonneg.Ring
-import Mathlib.Algebra.Order.Archimedean
 
 #align_import algebra.order.nonneg.floor from "leanprover-community/mathlib"@"b3f4f007a962e3787aa0f3b5c7942a1317f7d88e"
 
@@ -25,12 +25,6 @@ namespace Nonneg
 
 variable {α : Type*}
 
-instance archimedean [OrderedAddCommMonoid α] [Archimedean α] : Archimedean { x : α // 0 ≤ x } :=
-  ⟨fun x y hy =>
-    let ⟨n, hr⟩ := Archimedean.arch (x : α) (hy : (0 : α) < y)
-    ⟨n, show (x : α) ≤ (n • y : { x : α // 0 ≤ x }) by simp [*, -nsmul_eq_mul, nsmul_coe]⟩⟩
-#align nonneg.archimedean Nonneg.archimedean
-
 instance floorSemiring [OrderedSemiring α] [FloorSemiring α] :
     FloorSemiring { r : α // 0 ≤ r } where
   floor a := ⌊(a : α)⌋₊
diff --git a/Mathlib/Data/Rat/NNRat.lean b/Mathlib/Data/Rat/NNRat.lean
index f6a7c4b1e29bf..20dc8409c5fcc 100644
--- a/Mathlib/Data/Rat/NNRat.lean
+++ b/Mathlib/Data/Rat/NNRat.lean
@@ -5,7 +5,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.Order.Nonneg.Field
-import Mathlib.Algebra.Order.Nonneg.Floor
+import Mathlib.Data.Int.Lemmas
 
 #align_import data.rat.nnrat from "leanprover-community/mathlib"@"b3f4f007a962e3787aa0f3b5c7942a1317f7d88e"
 
@@ -40,7 +40,6 @@ def NNRat := { q : ℚ // 0 ≤ q } deriving
 -- instead of `deriving` them
 instance : OrderedSub NNRat := Nonneg.orderedSub
 instance : DenselyOrdered NNRat := Nonneg.densely_ordered
-instance : Archimedean NNRat := Nonneg.archimedean
 
 -- mathport name: nnrat
 scoped[NNRat] notation "ℚ≥0" => NNRat

From 7a839c06d9e0b3fdf4063bd1ea1649003727b846 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 24 Jan 2024 00:29:46 +0000
Subject: [PATCH 2/2] long lines

---
 Mathlib/Algebra/Order/Archimedean.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Order/Archimedean.lean b/Mathlib/Algebra/Order/Archimedean.lean
index 1a4ba8bde7bf1..7a41c7c18de0d 100644
--- a/Mathlib/Algebra/Order/Archimedean.lean
+++ b/Mathlib/Algebra/Order/Archimedean.lean
@@ -410,7 +410,8 @@ instance : Archimedean ℤ :=
 instance : Archimedean ℚ :=
   archimedean_iff_rat_le.2 fun q => ⟨q, by rw [Rat.cast_id]⟩
 
-instance Nonneg.archimedean [OrderedAddCommMonoid α] [Archimedean α] : Archimedean { x : α // 0 ≤ x } :=
+instance Nonneg.archimedean [OrderedAddCommMonoid α] [Archimedean α] :
+    Archimedean { x : α // 0 ≤ x } :=
   ⟨fun x y hy =>
     let ⟨n, hr⟩ := Archimedean.arch (x : α) (hy : (0 : α) < y)
     ⟨n, show (x : α) ≤ (n • y : { x : α // 0 ≤ x }) by simp [*, -nsmul_eq_mul, nsmul_coe]⟩⟩