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.