[Merged by Bors] - chore: improvements to Presheaf simp lemmas#9542
Closed
[Merged by Bors] - chore: improvements to Presheaf simp lemmas#9542
Conversation
8 tasks
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jan 8, 2024
Various things break in the simpset for `Presheaf` when the simp algorithm changes in leanprover/lean4#3124. These backwards compatible fixes are, I think, improvements anyway. One could further add a `Presheaf.id_app` lemma, and do further cleanup in the proofs which now use `dsimp [-Presheaf.comp_app]`, but I'd prefer if these are done in a followup PR in order to not hold up #9500. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Various things break in the simpset for
Presheafwhen the simp algorithm changes in leanprover/lean4#3124. These backwards compatible fixes are, I think, improvements anyway.One could further add a
Presheaf.id_applemma, and do further cleanup in the proofs which now usedsimp [-Presheaf.comp_app], but I'd prefer if these are done in a followup PR in order to not hold up #9500.