V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X Y Z : Action V G
⊢ ((𝟙 X.V ⊗ 𝟙 (Y.V ⊗ Z.V)) ≫ (α_ X.V Y.V Z.V).inv) ≫ (𝟙 (X.V ⊗ Y.V) ⊗ 𝟙 Z.V) = (α_ X.V Y.V Z.V).inv
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X Y Z : Action V G
⊢ (α_ X Y Z).inv.hom = (α_ X.V Y.V Z.V).inv
dsimp [Monoidal.transport_associator]
no goals
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X Y Z : Action V G
⊢ ((𝟙 X.V ⊗ 𝟙 (Y.V ⊗ Z.V)) ≫ (α_ X.V Y.V Z.V).inv) ≫ (𝟙 (X.V ⊗ Y.V) ⊗ 𝟙 Z.V) = (α_ X.V Y.V Z.V).inv
simp