chore(*): `LinearOrder` + `IsWellOrder α (· < ·)` → `LinearOrder` + `WellFoundedLT`

[vihdzp]

These hypotheses are equivalent, but the former spelling contains duplicated hypotheses throughout both typeclasses.

---

• [x] depends on: #15904

[github-actions[bot]]

PR summary e8d84d6504

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.RelClasses	137	123	-14 (-10.22%)

Import changes for all files

Files	Import difference
3 files Mathlib.Order.RelClasses Mathlib.Data.Sigma.Lex Mathlib.Deprecated.RelClasses	-14
Mathlib.Order.RelIso.Basic	-11
Mathlib.Order.RelIso.Group	-8

---

Declarations diff

+ instance (priority := 100) isWellOrder_gt [LinearOrder α] [WellFoundedGT α] : + instance (priority := 100) isWellOrder_lt [LinearOrder α] [WellFoundedLT α] : + instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, LinearOrder (β a)] : + instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, PartialOrder (β a)] + instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderBot (β a)] : + instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderTop (β a)] : + instance [WellFoundedLT I] : WellFoundedLT (Products I) := by + wellFoundedLT_toType_lt ++ instance [LinearOrder ι] [WellFoundedLT ι] [Nonempty ι] [∀ i, PartialOrder (β i)] - Nat.lt.isWellOrder - instIsWellOrder - instance (priority := 10) LinearOrder.isWellOrder_gt [LinearOrder α] : IsWellOrder α (· > ·) := {} - instance (priority := 10) LinearOrder.isWellOrder_lt [LinearOrder α] : IsWellOrder α (· < ·) := {} - instance : IsWellOrder NONote (· < ·) - instance : IsWellOrder NatOrdinal (· < ·) - instance : IsWellOrder Nimber (· < ·) - instance : IsWellOrder ℕ∞ (· < ·) - instance [IsWellOrder I (· < ·)] : IsWellFounded (Products I) (·<·) := by - instance [LinearOrder α] [h : IsWellOrder α (· < ·)] : IsWellOrder αᵒᵈ (· > ·) := h - instance [LinearOrder α] [h : IsWellOrder α (· > ·)] : IsWellOrder αᵒᵈ (· < ·) := h - instance [LinearOrder ι] [IsWellOrder ι (· < ·)] [∀ a, LinearOrder (β a)] : - instance [LinearOrder ι] [IsWellOrder ι (· < ·)] [∀ a, PartialOrder (β a)] - instance [LinearOrder ι] [IsWellOrder ι (· < ·)] [∀ a, PartialOrder (β a)] [∀ a, OrderBot (β a)] : - instance [LinearOrder ι] [IsWellOrder ι (· < ·)] [∀ a, PartialOrder (β a)] [∀ a, OrderTop (β a)] : - isWellOrder_toType_lt - wo -- instance [LinearOrder ι] [IsWellOrder ι (· < ·)] [Nonempty ι] [∀ i, PartialOrder (β i)] -- isWellOrder

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

[vihdzp]

!bench

[leanprover-bot]

Here are the benchmark results for commit 372d333b385501ee4f142e31234c800de3270598. There were significant changes against commit fc157081b3adaa6877bf68c0415d54c0126cf47f:

  Benchmark   Metric                 Change
  =========================================
- build       .olean serialization    13.4%
- build       import                  12.4%
- build       initialization          10.1%

[github-actions[bot]]

File	Instructions	%
build	-39.17⬝10⁹	(-0.2%)
lint	-9.765⬝10⁹	(-0.14%)
Mathlib.Topology.Category.Profinite.Nobeling	+1.879⬝10⁹	(+1.67%)

2 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody	-1.129⬝10⁹	(-0.68%)
Mathlib.Order.RelClasses	-1.606⬝10⁹	(-12.19%)

File	Instructions	%
Mathlib.Analysis.FunctionalSpaces.SobolevInequality	-2.760⬝10⁹	(-1.72%)
Mathlib.CategoryTheory.SmallObject.Iteration	-3.560⬝10⁹	(-18.58%)

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

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

[vihdzp]

!bench

[leanprover-bot]

Here are the benchmark results for commit 83ffff71cbc13f13ace0b382a26ad01cfc584590. There were no significant changes against commit 970d241d0868926adcfcc688a4a2b846fe732ea3.

[github-actions[bot]]

File	Instructions	%
build	-28.921⬝10⁹	(-0.2%)
lint	-9.605⬝10⁹	(-0.14%)

2 files, Instructions +1.0⬝10⁹

File	Instructions	%
Mathlib.Topology.Category.Profinite.Nobeling	+1.975⬝10⁹	(+1.76%)
Mathlib.MeasureTheory.Measure.FiniteMeasure	+1.665⬝10⁹	(+2.25%)

2 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody	-1.199⬝10⁹	(-0.72%)
Mathlib.Order.RelClasses	-1.606⬝10⁹	(-12.19%)

File	Instructions	%
Mathlib.Analysis.FunctionalSpaces.SobolevInequality	-2.749⬝10⁹	(-1.72%)

[vihdzp]

I've thought about this, but it seems a bit messy given that LinearOrder carries a lot of data (the ≤ relationship, maximums and minimums, decidability instances...) that isn't really needed.

We can instead expose induction and recursion principles that use LinearOrder + WellFoundedLT, and in fact I've already done that in a branch I plan to PR in the near future.

By the way, I didn't actually remove any instances. I added an instance LinearOrder + WellFoundedLT -> IsWellOrder that made the instances I deleted redundant. (Note that this instance would have looped in Lean 3, but Lean 4 seems to have no problem with this)

[alreadydone]

I see, it's just these two instances that can no longer be synthesized.

maintainer merge

[github-actions[bot]]

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

[vihdzp]

Oh, removing those instances was a mistake. But if they're not used, I think it's fine to have them removed since you shouldn't be using IsWellOrder α (· < ·) anyways...

[urkud]

Thanks! :tada: bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style