Commit 2024-01-08 11:01 afe6b29f
View on Github →chore: improvements to Presheaf simp lemmas (#9542)
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.