Commit 2025-02-19 17:41 b66f518c
View on Github →refactor(Tactic/CategoryTheory): generate ConcreteCategory lemmas in elementwise (#21729)
This should be the last big step in going from HasForget to ConcreteCategory: modifying the elementwise metaprogram so by default it emits lemmas spelled in the language of ConcreteCategory.