[Merged by Bors] - feat: pushing Lattice and predecessors through Equiv

[Parcly-Taxel]

The point is to transfer as cheaply as possible instances over to type synonyms. Note that we already have these for most of the algebraic hierarchy even when they "generalise" from an equiv to a structure-preserving injective function (note that the equiv needn't be structure-preserving, precisely because said structure needn't exist already).

[github-actions]

PR summary cd8272a9d5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ distribLattice
+ lattice
+ le
+ le_def
+ linearOrder
+ lt
+ lt_def
+ max
+ max_def
+ min
+ min_def
+ ord
+ ord_def
+ partialOrder
+ preorder
+ semilatticeInf
+ semilatticeSup

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[vihdzp]

Doesn't this just duplicate what we can already do with the Function.Injective constructors?

[Parcly-Taxel]

Doesn't this just duplicate what we can already do with the Function.Injective constructors?

Yaël asked me to do this. See #36934 (comment).

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

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

[riccardobrasca]

I didn't check if really all the declarations work in the case of an injective function, but I agree with @vihdzp that it's not clear why we want this. @YaelDillies if you have a good reason can you explain this in the PR description (and maybe also in the code)? Thanks!

[YaelDillies]

The point is to transfer as cheaply as possible instances over to type synonyms. Note that we already have these for most of the algebraic hierarchy even when they "generalise" from an equiv to a structure-preserving injective function (note that the equiv needn't be structure-preserving, precisely because said structure needn't exist already).

[JovanGerb]

Have we thought about potentially automating this, instead of writinf these instances out explicitly? (I don't want to block this PR, but it may be interesting to think about)

I find that the intros <;> rfl is a bit unnecessary, shouldn't we use autoparams instead (and then not use tactic mode in these instancea)?

[YaelDillies]

I would be very happy for automation to exist here, but note that what Jeremy's PR is doing is merely extending the statu quo and we shouldn't block him on that.

Also note that ideas for such automation have in the past systematically been shot down on the same basis as Violeta and Riccardo's objection above.

[faenuccio]

I agree with @riccardobrasca that a bit of details in the PR description would help before merging.

[YaelDillies]

Have added my comment above as description

[faenuccio]

Thanks.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job
• ci (staging) / Lint style