[Merged by Bors] - feat: Std.Total instance for InvImage

[kim-em]

This PR fills in the transfer of unbundled relation classes along InvImage and Order.Preimage, so that both spellings carry everything Function.onFun already has.

InvImage gains Std.Refl, Std.Symm, Std.Asymm, Std.Total, IsPreorder, IsEquiv, IsStrictOrder and IsStrictWeakOrder instances, along with antisymm, trichotomous, isPartialOrder, isLinearOrder and isStrictTotalOrder for injective f. (Std.Irrefl and IsTrans are already in Mathlib/Order/Defs/Unbundled.lean.) These are stated for Sort, matching core's InvImage. Order.Preimage gains the four injectivity lemmas trichotomous, isPartialOrder, isLinearOrder and isStrictTotalOrder.

All of these are definitionally the Function.onFun versions, and are proved by inferInstanceAs, but instance search does not fire on goals stated with InvImage or ⁻¹'o (and InvImage is how goals arise from WellFoundedRelation-adjacent and Sum.Lex-based constructions). Used in leanprover/cslib#401.

example {α β : Type} (r : α → α → Prop) [Std.Total r] (f : β → α) :
    Std.Total (InvImage r f) := inferInstance

🤖 Prepared with Claude Code

[github-actions]

PR summary 27adedc5c9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ antisymm
+ asymm
+ isEquiv
+ isPreorder
+ isStrictOrder
+ isStrictWeakOrder
+ refl
+ symm
+ total
++ isLinearOrder
++ isPartialOrder
++ isStrictTotalOrder
++ trichotomous
- InvImage.asymm
- InvImage.trichotomous

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 27adedc).

• +15 new declarations
• −0 removed declarations

+InvImage.antisymm
+InvImage.isEquiv
+InvImage.isLinearOrder
+InvImage.isPartialOrder
+InvImage.isPreorder
+InvImage.isStrictOrder
+InvImage.isStrictTotalOrder
+InvImage.isStrictWeakOrder
+InvImage.refl
+InvImage.symm
+InvImage.total
+Order.Preimage.isLinearOrder
+Order.Preimage.isPartialOrder
+Order.Preimage.isStrictTotalOrder
+Order.Preimage.trichotomous

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 27adedc5c9
Reference commit 1318ddb253

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[SnirBroshi]

Can you add the rest? Function.onFun has all of the instances, including the ones that require injectiveness, so we should translate all of those to both Order.Preimage and InvImage.

If you could generalize core's InvImage from Prop to any sort we'll also be able to deprecate the other two.
#mathlib4 > `Order.Preimage` vs `Function.onFun`

[kim-em]

If you could generalize core's InvImage from Prop to any sort we'll also be able to deprecate the other two.
#mathlib4 > Order.Preimage vs Function.onFun

Definitely out of scope for today. :-)

[kim-em]

Can you add the rest? Function.onFun has all of the instances, including the ones that require injectiveness, so we should translate all of those to both Order.Preimage and InvImage.

Personally, I think it is not a good idea to ask for scope creep in reviews. It slows everything down unnecessarily. Nevertheless, I'll do these now.

[eric-wieser]

bors merge

Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

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