C✝ : Type u
𝒞 : Category C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ 𝟙 Z ⊗ f ≫ g = 𝟙 Z ≫ 𝟙 Z ⊗ f ≫ g
C✝ : Type u
𝒞 : Category C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ 𝟙 Z ⊗ f ≫ g = (𝟙 Z ⊗ f) ≫ (𝟙 Z ⊗ g)
rw [← tensor_comp]
no goals
C✝ : Type u
𝒞 : Category C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ 𝟙 Z ⊗ f ≫ g = 𝟙 Z ≫ 𝟙 Z ⊗ f ≫ g
simp