Commit 2025-02-02 12:17 67a5732f

View on Github →

perf(CategoryTheory/Shift/Induced): remove @[simp] from shiftFunctor_of_induced (#21329) This PR removes the simp tag from shiftFunctor_of_induced. This lemma isn't used, and it has a very unfavourable discrimination tree key, meaning that it is tried every time the constant shiftFunctor appears.

Estimated changes