mathlib3

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

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:  After:  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>