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✝ V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ inv f) ≫ (h ⊗ f) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)
rw [← tensor_comp, IsIso.inv_hom_id, comp_tensor_id]