Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(category_theory): simps should not add hom lemmas#18742

Closed
kim-em wants to merge 2 commits intomasterfrom
simps_hom
Closed

[Merged by Bors] - chore(category_theory): simps should not add hom lemmas#18742
kim-em wants to merge 2 commits intomasterfrom
simps_hom

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Apr 5, 2023

@[simps] should not be used to simplify the hom field of a category instance.

Very little needs to be changed when removing it.

However the problem in leanprover-community/mathlib4#3244 with a proof by simp failing seems to be implicated by this problem. If we remove the @[simps] generated lemma for Hom there, the original proof works (although is extremely slow).

Open in Gitpod

@kim-em kim-em added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Apr 5, 2023
@kim-em kim-em requested a review from a team as a code owner April 5, 2023 11:09
fpvandoorn
fpvandoorn reviewed Apr 5, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

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

seems reasonable

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Apr 5, 2023

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

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 5, 2023
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Apr 8, 2023

bors p=10

@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Apr 8, 2023

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Apr 8, 2023

👎 Rejected by label

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-CI The author would like to see what CI has to say before doing more work. labels Apr 8, 2023
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Apr 8, 2023

bors merge

bors bot pushed a commit that referenced this pull request Apr 8, 2023
@kim-em
chore(category_theory): simps should not add hom lemmas (#18742)
2efd242 
`@[simps]` should not be used to simplify the `hom` field of a category instance.

Very little needs to be changed when removing it.

However the problem in leanprover-community/mathlib4#3244 with a proof by `simp` failing seems to be implicated by this problem. If we remove the `@[simps]` generated lemma for `Hom` there, the original proof works (although is extremely slow).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@kim-em kim-em mentioned this pull request Apr 8, 2023
Closed
@bors
Copy link
Copy Markdown

bors bot commented Apr 8, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(category_theory): simps should not add hom lemmas [Merged by Bors] - chore(category_theory): simps should not add hom lemmas Apr 8, 2023
@bors bors bot closed this Apr 8, 2023
@bors bors bot deleted the simps_hom branch April 8, 2023 13:17
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 10, 2023
@kim-em @joelriou
chore: forward port of #18742, no simps lemmas for Category.Hom (#3340)
18229dc 
This is the forward port of leanprover-community/mathlib3#18742. That PR hasn't landed yet, so this PR still needs to be updated with the new commit SHA.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 10, 2023
@kim-em @joelriou
chore: forward port of #18742, no simps lemmas for Category.Hom (#3340)
fa79900 
This is the forward port of leanprover-community/mathlib3#18742. That PR hasn't landed yet, so this PR still needs to be updated with the new commit SHA.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 10, 2023
@kim-em @joelriou
chore: forward port of #18742, no simps lemmas for Category.Hom (#3340)
e44913f 
This is the forward port of leanprover-community/mathlib3#18742. That PR hasn't landed yet, so this PR still needs to be updated with the new commit SHA.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
@Parcly-Taxel Parcly-Taxel mentioned this pull request Apr 11, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 11, 2023
@Parcly-Taxel
chore: forward port mathlib#17611, 18742, 18198, 18520 (#3389)
13413a3 
SHA-only updates:
* leanprover-community/mathlib3#17611 – `CategoryTheory.Sites.Sheaf` already uses `aesop_cat` at this location, nothing to port.
* leanprover-community/mathlib3#18742 – fiber spelling, which is all of the changes to `Topology.FiberBundle.Trivialization`, is already in mathlib4.
* leanprover-community/mathlib3#18198 – `FunLike` change to `Data.PEquiv` is already in mathlib4.

Substantative forward port:
* leanprover-community/mathlib3#18520



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
eric-wieser pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 12, 2023
@Parcly-Taxel
chore: forward port mathlib#17611, 18742, 18198, 18520 (#3389)
84169f4 
SHA-only updates:
* leanprover-community/mathlib3#17611 – `CategoryTheory.Sites.Sheaf` already uses `aesop_cat` at this location, nothing to port.
* leanprover-community/mathlib3#18742 – fiber spelling, which is all of the changes to `Topology.FiberBundle.Trivialization`, is already in mathlib4.
* leanprover-community/mathlib3#18198 – `FunLike` change to `Data.PEquiv` is already in mathlib4.

Substantative forward port:
* leanprover-community/mathlib3#18520



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@fpvandoorn fpvandoorn fpvandoorn left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kim-em @fpvandoorn @leanprover-community-bot-assistant