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✝ W X Y Z : C
⊢ inv ((𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ 𝟙 Z)) =
    inv ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv)
simp [pentagon]