Commit 2024-01-08 11:01 afe6b29f

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.