Commit 2022-11-11 04:41 cead9313

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.)