no goals
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
⊢ tensorHom (associator W X Y).hom (𝟙 Z) ≫
      (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
    (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom
convert pentagon_aux R W X Y Z using 1