Skip to content

feat(Order/RelIso): add lemmas about congruence with relIso#37640

Open
IvanRenison wants to merge 5 commits intoleanprover-community:masterfrom
IvanRenison:RelIso.relIsoCongr
Open

feat(Order/RelIso): add lemmas about congruence with relIso#37640
IvanRenison wants to merge 5 commits intoleanprover-community:masterfrom
IvanRenison:RelIso.relIsoCongr

Conversation

@IvanRenison
Copy link
Copy Markdown
Collaborator

@IvanRenison IvanRenison commented Apr 4, 2026 •
edited by Komyyy
Loading

Also, the default simps lemmas (*_apply and *_symm_apply) are convenient for simp but not for rw, simp_rw, or simp_only, so we add new simps lemmas for them (*_apply_apply and *_symm_apply_apply).

In #37598 I realized this is missing

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 4, 2026 •
edited
Loading

PR summary 6b3e5a3312

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ relEmbeddingCongr
+ relIsoCongr

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

@github-actions github-actions bot added the t-order Order theory label Apr 4, 2026
@IvanRenison IvanRenison mentioned this pull request Apr 5, 2026
Open
5 tasks
Komyyy
Komyyy requested changes Apr 9, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for your contribution!

Comment thread Mathlib/Order/RelIso/Basic.lean Outdated
Comment thread Mathlib/Order/RelIso/Basic.lean Outdated
@Komyyy Komyyy added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 9, 2026
@IvanRenison IvanRenison removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 9, 2026
Komyyy
Komyyy requested changes Apr 11, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These are my final reviews.

Comment thread Mathlib/Order/RelIso/Basic.lean
@@ -772,6 +772,32 @@ def relHomCongr {α₁ β₁ α₂ β₂}
left_inv f₁ := by ext; simp
right_inv f₂ := by ext; simp

Copy link
Copy Markdown
Contributor

@Komyyy Komyyy Apr 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I found that the generated simps lemmas are convenient for simp but not for rw, simp only and simp_rw.
Could you add new simps lemmas for rws, and mention this in the PR message?

Suggested change
attribute [simps! -isSimp apply_apply symm_apply_apply] relHomCongr

Copy link
Copy Markdown
Collaborator Author

@IvanRenison IvanRenison Apr 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure to understand. I added the attribute lines, I'm not sure if I should add something more, and I'm not sure exactly what to say in the PR message?

Copy link
Copy Markdown
Contributor

@Komyyy Komyyy Apr 18, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry for the late reply! I've been busy lately.

I've updated your PR message.

Comment thread Mathlib/Order/RelIso/Basic.lean
Comment thread Mathlib/Order/RelIso/Basic.lean
Comment thread Mathlib/Order/RelIso/Basic.lean Outdated
Comment thread Mathlib/Order/RelIso/Basic.lean Outdated
Comment thread Mathlib/Order/RelIso/Basic.lean Outdated
@Komyyy Komyyy added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 11, 2026
@IvanRenison IvanRenison removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 11, 2026
Komyyy
Komyyy approved these changes Apr 18, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you!

maintainer merge

Comment thread Mathlib/Order/RelIso/Basic.lean
@@ -772,6 +772,32 @@ def relHomCongr {α₁ β₁ α₂ β₂}
left_inv f₁ := by ext; simp
right_inv f₂ := by ext; simp

Copy link
Copy Markdown
Contributor

@Komyyy Komyyy Apr 18, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry for the late reply! I've been busy lately.

I've updated your PR message.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 18, 2026

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

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 18, 2026
@Komyyy Komyyy removed their assignment Apr 18, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Komyyy Komyyy Komyyy approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@IvanRenison @Komyyy