refactor: move Archimedean instances to Order/Archimedean (#9950)

We already have the instances for `ℕ`, `ℤ`, and `ℚ` in this file, so adding `NNRat` doesn't feel that out of place, as it completes this {negation,division} lattice.

Follows on from #9917. These changes knock off 132 dependencies from `NNRat`, though adds more to `Archimedean`.
I think this is acceptable; we need `NNRat` to be super early if we want to be able to use it in norm_num, and the depth of `Archimedean` will reduce with `NNRat` as I work towards this.

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,15 @@ 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 α :=

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 : α)⌋₊

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