[Merged by Bors] - feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right by sgouezel · Pull Request #25604 · leanprover-community/mathlib4

sgouezel · 2025-06-08T19:20:16Z

This follows the usual convention for coercions. See discussion at #mathlib4 > simp normal form for symm and coercions @ 💬

For each equiv class, after the PR we should have lemmas like

@[simp]
lemma coe_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv = e := rfl

@[simp]
lemma coe_symm_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv.symm = e.symm := rfl

@[simp]
lemma toEquiv_symm (e : G ≃+c[a, b] H) : e.symm.toEquiv = e.toEquiv.symm := rfl

@[simp]
lemma toEquiv_trans (e₁ : G ≃+c[a, b] H) (e₂ : H ≃+c[b, c] K) :
    (e₁.trans e₂).toEquiv = e₁.toEquiv.trans e₂.toEquiv := rfl

The PR does not complete this task, because it would require killing the coercion from EquivLike classes to Equivs (which I am planning to do in a subsequent PR), but it is a significant first step in this direction.

github-actions · 2025-06-08T19:21:31Z

PR summary c34d6acfe2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ _root_.IsometryEquiv.coe_symm_toDilationEquiv
+ _root_.IsometryEquiv.coe_toDilationEquiv
+ coe_mk
+ coe_symm_toContinuousLinearEquiv
+ coe_symm_toIntLinearEquiv
+ coe_symm_toMeasurableEquiv
+ coe_symm_toNatLinearEquiv
+ coe_symm_toRelIsoLT
+ coe_toLinearEquiv
+ coe_toRelIsoLT
+ linear_symm
+ toContinuousLinearEquiv_symm
+ toEquiv_trans
+ toHomeomorph_trans
+ toIsometryEquiv_trans
++ coe_symm_toAffineEquiv
++ coe_symm_toIsometryEquiv
+++ coe_symm_toLinearEquiv
+++ coe_toEquiv
++++ coe_symm_toHomeomorph
+++++++ coe_symm_toEquiv
++++-+++ toEquiv_symm
+++--- coe_toEquiv_symm
++- toAffineEquiv_symm
++-- toIsometryEquiv_symm
+-+++-- toHomeomorph_symm
+-++- toLinearEquiv_symm

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.

No changes to technical debt.

You can run this locally as

./scripts/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).

j-loreaux · 2025-06-11T00:57:49Z

killing the coercion from EquivLike classes to Equivs

You're planning on killing it as a coercion, but keeping the constructor, right?

j-loreaux

Thanks for making all these consistent!

Mathlib/Algebra/Module/Equiv/Defs.lean

Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

Mathlib/Order/Hom/Basic.lean

Mathlib/RingTheory/Bialgebra/Equiv.lean

Mathlib/RingTheory/Coalgebra/Equiv.lean

Mathlib/Topology/Algebra/Module/Equiv.lean

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

j-loreaux · 2025-06-11T22:32:08Z

@sgouezel I won't merge in case there was a reason you didn't take the awaiting-author tag off. But in case you're done:

bors d+

mathlib-bors · 2025-06-11T22:32:10Z

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

sgouezel · 2025-06-12T07:25:26Z

bors r+
Thanks a lot for the careful review!

…s `symm` and `trans` to the right (#25604) This follows the usual convention for coercions. See discussion at [#mathlib4 > simp normal form for symm and coercions @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/simp.20normal.20form.20for.20symm.20and.20coercions/near/522879475) For each equiv class, after the PR we should have lemmas like ```lean @[simp] lemma coe_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv = e := rfl @[simp] lemma coe_symm_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv.symm = e.symm := rfl @[simp] lemma toEquiv_symm (e : G ≃+c[a, b] H) : e.symm.toEquiv = e.toEquiv.symm := rfl @[simp] lemma toEquiv_trans (e₁ : G ≃+c[a, b] H) (e₂ : H ≃+c[b, c] K) : (e₁.trans e₂).toEquiv = e₁.toEquiv.trans e₂.toEquiv := rfl ``` The PR does not complete this task, because it would require killing the coercion from EquivLike classes to Equivs (which I am planning to do in a subsequent PR), but it is a significant first step in this direction.

mathlib-bors · 2025-06-12T08:56:37Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* master: (447 commits) chore(Data/Set): move very basic lemmas earlier (leanprover-community#25707) feat: preserve draft status when migrating PRs to fork (leanprover-community#25777) chore(Data/Set/Basic): deprecate lemmas that abuse the `Set α := α → Prop` defeq (leanprover-community#25669) refactor: redefine `ProperCone` as an `abbrev` for `ClosedSubmodule` (leanprover-community#25204) feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (leanprover-community#25564) fix: outdated docstring (leanprover-community#25717) feat(MeasureTheory): convolution of measures with densities (leanprover-community#25718) feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right (leanprover-community#25604) feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948) feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (leanprover-community#25333) fix: typo in labels_from_comment.yml (leanprover-community#25727) feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705) feat: check that the mathlib options exist (leanprover-community#25687) feat(Algebra/Group/Even): Add missing lemmas (leanprover-community#20818) refactor: make `Matrix.kroneckerTMulAlgEquiv` heterogeneous (leanprover-community#25693) feat: allow contributors to remove labels with comments (leanprover-community#25723) chore: disable build.yml and bors.yml on forks (leanprover-community#25722) feat: improvements to user_activity_report.py (leanprover-community#25721) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) ...

…s `symm` and `trans` to the right (leanprover-community#25604) This follows the usual convention for coercions. See discussion at [#mathlib4 > simp normal form for symm and coercions @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/simp.20normal.20form.20for.20symm.20and.20coercions/near/522879475) For each equiv class, after the PR we should have lemmas like ```lean @[simp] lemma coe_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv = e := rfl @[simp] lemma coe_symm_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv.symm = e.symm := rfl @[simp] lemma toEquiv_symm (e : G ≃+c[a, b] H) : e.symm.toEquiv = e.toEquiv.symm := rfl @[simp] lemma toEquiv_trans (e₁ : G ≃+c[a, b] H) (e₂ : H ≃+c[b, c] K) : (e₁.trans e₂).toEquiv = e₁.toEquiv.trans e₂.toEquiv := rfl ``` The PR does not complete this task, because it would require killing the coercion from EquivLike classes to Equivs (which I am planning to do in a subsequent PR), but it is a significant first step in this direction.

sgouezel added 15 commits June 7, 2025 19:31

start

687a987

fix

5221ca3

more

08ed103

more

88f4969

fix

fd9d225

fix

a99dbe9

fix

8966b9b

fix

357245c

fix

130bcd7

fix

adaec39

fix

426ffb9

fix

ebe5e2d

fix

3b1ae16

lint

bb19571

fix

07998bf

sgouezel added the WIP Work in progress label Jun 8, 2025

sgouezel added 3 commits June 8, 2025 21:35

deprecations

a263339

deprecations

25f6a31

cleanup

7a08df4

sgouezel removed the WIP Work in progress label Jun 8, 2025

j-loreaux reviewed Jun 11, 2025

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 11, 2025

sgouezel and others added 4 commits June 11, 2025 18:28

Update Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

fbaf610

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Update Mathlib/Order/Hom/Basic.lean

0c3c403

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Merge remote-tracking branch 'origin/master' into SG_moveSymm

936439b

deprecate without aliases

551a69c

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 11, 2025

fix

9d30fb9

ghost added the ready-to-merge This PR has been sent to bors. label Jun 12, 2025

mathlib-bors bot changed the title ~~feat: make sure that the simp normal form of equiv-like classes pushes symm and trans to the right~~ [Merged by Bors] - feat: make sure that the simp normal form of equiv-like classes pushes symm and trans to the right Jun 12, 2025

mathlib-bors bot closed this Jun 12, 2025

mathlib-bors bot deleted the SG_moveSymm branch June 12, 2025 08:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right#25604

[Merged by Bors] - feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right#25604
sgouezel wants to merge 23 commits intomasterfrom
SG_moveSymm

sgouezel commented Jun 8, 2025

Uh oh!

github-actions bot commented Jun 8, 2025 •

edited

Loading

Declarations diff

Uh oh!

j-loreaux commented Jun 11, 2025

Uh oh!

j-loreaux left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

j-loreaux commented Jun 11, 2025

Uh oh!

mathlib-bors bot commented Jun 11, 2025

Uh oh!

sgouezel commented Jun 12, 2025

Uh oh!

mathlib-bors bot commented Jun 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

sgouezel commented Jun 8, 2025

Uh oh!

github-actions bot commented Jun 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c34d6acfe2

Import changes for modified files

Declarations diff

Uh oh!

j-loreaux commented Jun 11, 2025

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

j-loreaux commented Jun 11, 2025

Uh oh!

mathlib-bors bot commented Jun 11, 2025

Uh oh!

sgouezel commented Jun 12, 2025

Uh oh!

mathlib-bors bot commented Jun 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions bot commented Jun 8, 2025 •

edited

Loading