[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ⊗≫ g = f ≫ g
[PROOFSTEP]
simp [monoidalComp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y : C
f : U ⟶ V ⊗ W ⊗ X
g : (V ⊗ W) ⊗ X ⟶ Y
⊢ f ⊗≫ g = f ≫ (α_ V W X).inv ≫ g
[PROOFSTEP]
simp [monoidalComp]
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : MonoidalCategory C✝
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
w : f ≫ 𝟙 Y = g
⊢ f = g
[PROOFSTEP]
simpa using w
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : MonoidalCategory C✝
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g ≫ 𝟙 Y
⊢ f = g
[PROOFSTEP]
simpa using w
