chore: Move Nat.instLinearOrder to Init.Order.Defs

[Ruben-VandeVelde]

It turns out that pushing the dependency out is quite annoying, so as an alternative, we propose considering Preorder, PartialOrder and LinearOrder to be foundational type classes that all of Mathlib can depend on.

---

[github-actions[bot]]

PR summary 1e4fa52b94

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Char	107	28	-79 (-73.83%)
Mathlib.Init.Order.Defs	37	13	-24 (-64.86%)
Mathlib.Init.Data.Int.Order	40	17	-23 (-57.50%)
Mathlib.Init.Order.LinearOrder	38	26	-12 (-31.58%)
Mathlib.Tactic.GCongr.Core	42	31	-11 (-26.19%)
Mathlib.Data.PNat.Defs	131	109	-22 (-16.79%)
Mathlib.Order.RelClasses	135	116	-19 (-14.07%)
Mathlib.Order.Basic	106	103	-3 (-2.83%)
Mathlib.Data.Nat.Defs	106	104	-2 (-1.89%)
Mathlib.Logic.Equiv.Basic	153	151	-2 (-1.31%)
Mathlib.Data.Tree.Get	205	204	-1 (-0.49%)

---

Declarations diff

+ Nat.instLinearOrder - instLinearOrder

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[YaelDillies]

Ahah! That's basically the criticism I had against #13082. I am perfectly happy with the revert.

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[kim-em]

I'm concerned about moving material into Init, when we are trying to get rid of all these files. Can we achieve your end here without backsliding on this?

[kim-em]

Further (this is less urgent, but flagging a medium-term concern) I am cautious about considering LinearOrder as fundamental --- it is clear that for programming purposes we are going to need a substantial revision of the treatment of decidable inequalities and typeclasses guaranteeing properties of these functions. No one as yet has a concrete design, but it's clear that radical changes are needed at some point. I would suspect that LinearOrder itself will need to be revised as part of this (and hopefully will become less necessary in some applications).

I don't think reorganizations like this PR really add to the difficulty of refactors like this, but I think it's worth keeping in mind.

[Ruben-VandeVelde]

The idea (as I understand it right now) is that we'd move this entire file into a new library (within this repository) for mathlib to depend on, so I didn't see much point in moving it out of Init at this point. I have no opinion on the programming treatment of ordering.

[kim-em]

Oh, I think the short term plan is actually the opposite, to move all of the content of the Init files out into Mathlib proper, and then delete them.

[kim-em]

I would love to start splitting out the bottom of Mathlib into separate libraries within the Mathlib repo, but as far as I understand this proposal is still foundering on the shoals of decision-making. :-)

[riccardobrasca]

What is the status of this?

[YaelDillies]

What about you move the instance to Data.Nat.Defs for now? This is THE file for foundational stuff about Nat.