-
Notifications
You must be signed in to change notification settings - Fork 259
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: Port CategoryTheory.Adjunction.Opposites #2424
Conversation
adamtopaz
commented
Feb 21, 2023
•
edited by jcommelin
Loading
edited by jcommelin
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Lint done. |
adjointOfOpAdjointOp_homEquiv_symm_apply | ||
|
||
-- Porting note: simpNF reports simplifying to itself here | ||
@[simp, nolint simpNF] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the linter was right to flag this theorem. The LHS is simplified to something that looks the same, but has some different implicit arguments somewhere. Consequently, a lemma with the exact same statement as this one is not proved by simp
even with this lemma marked as a simp
lemma. I think this theorem is pretty useless until the LHS is in normal form including implicits.
….Adjunction.Opposites
homEquiv := fun {X Y} => | ||
((h.homEquiv (Opposite.op Y) (Opposite.op X)).trans (opEquiv _ _)).symm.trans | ||
(opEquiv _ _) | ||
homEquiv_naturality_left_symm := by |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would have hope there was a porting note here noting the regression that this proof is needed at all!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done!
The problematic lemmas generated by |
… lemmas (#18680) Some of the lemmas generated by `simps` in leanprover-community/mathlib4#2424 are bad according to the simpNF linter, and have proved hard to fix by hand. Fortunately, they are simply not needed. This PR verifies this by backporting their removal to mathlib3. Compiles locally, lets hope CI agrees. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors merge |
Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
* [`category_theory.adjunction.opposites`@`f3ee4628e2dc737653af924c41fa681abc2a4f4a`..`0148d455199ed64bf8eb2f493a1e7eb9211ce170`](https://leanprover-community.github.io/mathlib-port-status/file/category_theory/adjunction/opposites?range=f3ee4628e2dc737653af924c41fa681abc2a4f4a..0148d455199ed64bf8eb2f493a1e7eb9211ce170) The changes in leanprover-community/mathlib#18680 were already part of #2424, so we just need to update the SHA. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
* [`category_theory.adjunction.opposites`@`f3ee4628e2dc737653af924c41fa681abc2a4f4a`..`0148d455199ed64bf8eb2f493a1e7eb9211ce170`](https://leanprover-community.github.io/mathlib-port-status/file/category_theory/adjunction/opposites?range=f3ee4628e2dc737653af924c41fa681abc2a4f4a..0148d455199ed64bf8eb2f493a1e7eb9211ce170) The changes in leanprover-community/mathlib#18680 were already part of #2424, so we just need to update the SHA. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
* [`category_theory.adjunction.opposites`@`f3ee4628e2dc737653af924c41fa681abc2a4f4a`..`0148d455199ed64bf8eb2f493a1e7eb9211ce170`](https://leanprover-community.github.io/mathlib-port-status/file/category_theory/adjunction/opposites?range=f3ee4628e2dc737653af924c41fa681abc2a4f4a..0148d455199ed64bf8eb2f493a1e7eb9211ce170) The changes in leanprover-community/mathlib#18680 were already part of #2424, so we just need to update the SHA. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>