refactor(*): simplifying import hierarchy up to dat.rat.order (#17435)

My apologies that this is essentially unreviewable. I promise not to have dropped anything. :-) I appreciate that big PRs are terrible, but if I can't get this stuff through CI in a timely manner I just can't work on this refactor.

This PR introduces some technical debt: the lemmas in `data.nat.basic` / `data.nat.order.basic` / `data.nat.order.lemmas` / `data.nat.lemmas` (and similarly for `data.int.*`) are a total mess, organised mainly by trying to reduce import dependency for `linear_ordered_field ℚ`. We're going to have to go back and reorganise these later.

Before:

![data rat order before](https://user-images.githubusercontent.com/477956/200711738-69cae67b-fdb7-4ce5-9a71-a871fb16acdd.png)

After:

![data rat order after](https://user-images.githubusercontent.com/477956/200711761-7382a13f-bae7-4e2a-bb9a-56f0894ebdff.png)

That's reduced the import depth for `data.rat.order` from 33 to 25.

(For reference a week ago it had been at 59.)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

archive/imo/imo2011_q5.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Alain Verberkmoes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alain Verberkmoes
 -/
-import data.int.dvd
+import data.int.dvd.basic
 
 /-!
 # IMO 2011 Q5

src/algebra/continued_fractions/computation/basic.lean

@@ -5,7 +5,7 @@ Authors: Kevin Kappelmann
 -/
 import algebra.order.floor
 import algebra.continued_fractions.basic
-import algebra.order.field.basic
+
 /-!
 # Computable Continued Fractions
 

src/algebra/euclidean_domain/instances.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Louis Carlin, Mario Carneiro
 -/
 import algebra.euclidean_domain.defs
-import data.nat.order
-import data.int.order
+import algebra.group_with_zero.units
+import data.nat.order.basic
+import data.int.order.basic
 
 /-!
 # Instances for Euclidean domains

src/algebra/group/prod.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
 -/
-import algebra.hom.equiv.units
+import algebra.hom.equiv.units.group_with_zero
 import algebra.group.opposite
 
 /-!

src/algebra/group/ulift.lean

@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import data.int.cast.defs
 import algebra.hom.equiv.basic
-import algebra.group_with_zero.basic
+import algebra.group_with_zero.inj_surj
 
 /-!
 # `ulift` instances for groups and monoids

src/algebra/group_power/lemmas.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import algebra.invertible
 import algebra.group_power.ring
+import algebra.order.monoid.with_top
 import data.nat.pow
 import data.int.cast.lemmas
 

src/algebra/group_power/order.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import algebra.order.ring.abs
+import algebra.order.with_zero
 import algebra.group_power.ring
 import data.set.intervals.basic
 
@@ -358,7 +359,7 @@ one_lt_pow_iff_of_nonneg ha (nat.succ_ne_zero _)
 
 @[simp] theorem pow_left_inj {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) :
   x ^ n = y ^ n ↔ x = y :=
-(@strict_mono_on_pow R _ _ Hnpos).inj_on.eq_iff Hxpos Hypos
+(@strict_mono_on_pow R _ _ Hnpos).eq_iff_eq Hxpos Hypos
 
 lemma lt_of_pow_lt_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
 lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h

src/algebra/group_power/ring.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import algebra.group_power.basic
+import algebra.group_with_zero.units
 import algebra.hom.ring
-import data.nat.order
+import data.nat.order.lemmas
 
 /-!
 # Power operations on monoids with zero, semirings, and rings