chore: drop order dependency from Data.Nat.Defs

[Ruben-VandeVelde]

---

• [ ] depends on: #13082

I tried to limit the scope as much as possible here; there's more in https://github.com/leanprover-community/mathlib4/compare/Nat-LinearOrder-2 and https://github.com/leanprover-community/mathlib4/compare/List.Basic-no-algebra

[YaelDillies]

I must say I've toyed with the idea myself but I'm not yet sure I like it.

The lemmas you're removing the dependencies on are very basic and boil down to easy-but-annoying-to-prove-on-the-fly tautologies.

I suspect the correct solution is to upstream those lemmas to Batteries using Batteries-specific typeclasses

[Ruben-VandeVelde]

That's certainly not a project I want to start on :)

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13082~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary 7a692b8cb9

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.GCongr.Core	42	19	-23 (-54.76%)
Mathlib.Data.Char	107	165	+58 (+54.21%)
Mathlib.Tactic.Zify	135	178	+43 (+31.85%)
Mathlib.Data.PNat.Defs	131	167	+36 (+27.48%)
Mathlib.Init.Order.Defs	37	45	+8 (+21.62%)
Mathlib.Data.Nat.Factorial.Basic	243	275	+32 (+13.17%)
Mathlib.Order.Monotone.Basic	164	147	-17 (-10.37%)
Mathlib.Data.List.Basic	261	287	+26 (+9.96%)
Mathlib.Data.Seq.Computation	264	290	+26 (+9.85%)
Mathlib.Data.Nat.PSub	186	204	+18 (+9.68%)
Mathlib.Order.RelClasses	135	122	-13 (-9.63%)
Mathlib.Data.Nat.Bits	190	208	+18 (+9.47%)
Mathlib.Data.Nat.Defs	106	101	-5 (-4.72%)
Mathlib.Data.Int.Defs	119	114	-5 (-4.20%)
Mathlib.Order.Lattice	167	160	-7 (-4.19%)
Mathlib.Data.Int.Cast.Basic	126	121	-5 (-3.97%)
Mathlib.Order.Nat	169	164	-5 (-2.96%)
Mathlib.Order.Estimator	202	198	-4 (-1.98%)
Mathlib.Combinatorics.Quiver.Arborescence	204	200	-4 (-1.96%)
Mathlib.Data.Rat.Defs	250	246	-4 (-1.60%)
Mathlib.Algebra.Order.Monoid.Unbundled.Pow	182	183	+1 (+0.55%)
Mathlib.Data.Nat.Order.Lemmas	198	199	+1 (+0.51%)
Mathlib.Data.Nat.Log	205	206	+1 (+0.49%)
Mathlib.Algebra.Order.Ring.Defs	207	208	+1 (+0.48%)
Mathlib.Algebra.Order.Group.Nat	210	211	+1 (+0.48%)
Mathlib.Data.Set.List	211	212	+1 (+0.47%)
Mathlib.Order.CompleteLattice	229	230	+1 (+0.44%)
Mathlib.Data.Fin.Basic	302	303	+1 (+0.33%)
Mathlib.Algebra.Associated	325	326	+1 (+0.31%)
Mathlib.Data.Nat.Dist	380	381	+1 (+0.26%)
Mathlib.Data.Nat.Upto	380	381	+1 (+0.26%)
Mathlib.Data.PNat.Basic	384	385	+1 (+0.26%)
Mathlib.Data.Nat.Cast.Order	385	386	+1 (+0.26%)
Mathlib.Data.Bool.Count	392	393	+1 (+0.26%)
Mathlib.Data.Nat.Prime	396	397	+1 (+0.25%)
Mathlib.Data.Set.Pointwise.Basic	400	401	+1 (+0.25%)
Mathlib.Data.Nat.SuccPred	409	410	+1 (+0.24%)

---

Declarations diff

+ Mathlib.Tactic.GCongr.exactLeOfLt + Nat.le_or_lt + lt.isWellOrder - Nat.lt.isWellOrder - exactLeOfLt

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>

[Ruben-VandeVelde]

I still think this is useful; it's a blocker for Data.List.Basic, among other things.