no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) = (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv
coherence