case hom_inv_id
C_1 : Type u
𝒞 : Category C_1
inst : MonoidalCategory C_1
C : Type u
inst_1 : Category C
inst_2 : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
inst_3 : IsIso f
g : Y ⟶ Z
inst_4 : IsIso g
⊢ (f ⊗ g) ≫ (inv f ⊗ inv g) = 𝟙 (W ⊗ Y)
C✝ : Type u
𝒞 : Category C✝
inst✝⁴ : MonoidalCategory C✝
C : Type u
inst✝³ : Category C
inst✝² : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
inst✝¹ : IsIso f
g : Y ⟶ Z
inst✝ : IsIso g
⊢ inv (f ⊗ g) = inv f ⊗ inv g
aesop_cat_nonterminal
no goals
case hom_inv_id
C_1 : Type u
𝒞 : Category C_1
inst : MonoidalCategory C_1
C : Type u
inst_1 : Category C
inst_2 : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
inst_3 : IsIso f
g : Y ⟶ Z
inst_4 : IsIso g
⊢ (f ⊗ g) ≫ (inv f ⊗ inv g) = 𝟙 (W ⊗ Y)
simp [← tensor_comp]