Commit 2024-01-31 07:01 ec497096
View on Github →feat(CategoryTheory/Monoidal): partially setting simp lemmas (#10061)
Extracted from #6307. The main reason why #6307 is so large is that many tensoring of identity morphisms that appear in mathlib should be replaced with whiskerings. This PR will leave this issue and deal with other parts. That is, we do not set id_tensorHom
and tensorHom_id
as simple lemmas at this moment, We can set them as simp lemmas locally to enable simple normal forms.