Carve out Algebra, Data and Order sublibraries

[YaelDillies]

trafficstars

The bottom part of mathlib is quite a mess. Algebra, data structures and order theory could be developed separately (at least for a while) but are not. Instead, "horizontal" imports keep happening between what would otherwise be three disjoint trees.

The main sources of trouble are

• Nat and Int, as they are ubiquitous. Their basic properties can be accessed through typeclass-mediated lemmas by importing Data.Nat.Basic and Data.Nat.Order.Basic. However this comes at the cost of importing basic algebra or basic algebraic order theory where unnecessary. Instead, we can use the Nat- and Int-specific lemmas provided by Std.
• Many pure algebraic/order theoretic/data structuresque files import non-pure algebraic/order theoretic/data structuresque files just to prove a few properties of an object defined in the non-pure file. In that case, the import can be reversed so that the pure file has pure imports.
• Misplaced files. Eg Polynomial, Real or Set.Icc are defined under Data. The solution is to simply move them to the correct top-level folder.

The purpose of this issue is to collect the PRs doing at least one of the above:

• #11601
• #11633
• #11653
• #11661
• #11711
• #11715
• #11716
• #11725
• #11729
• #11732
• #11741
• #11750
• #11751
• #11753

Once all these issues will be fixed, we will be able to create three new Lean libraries Algebra, Data, Order, all still living in the current repository.

After such a split, these sublibraries would form a DAG in terms of dependencies. This adds some constraints to future refactors, as that DAG would essentially become immutable.

The benefits?

• working towards it requires drastically cleaning up the import graph, which currently is full of "horizontal gene transfer".
• the sublibrary DAG being immutable is also helpful: it prevents some dependency regressions!
• even though everything will remain in one repository (this is important to minimise the cost of cross-repository refactors), it will be possible in lake to specify that you only want to depend on a subset of these libraries.