∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : Cᴹᵒᵖ} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) (h : X₃ ⟶ Y₃),
  (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom h.unmop
            (CategoryTheory.MonoidalCategoryStruct.tensorHom g.unmop f.unmop).mop.unmop).mop
        (CategoryTheory.MonoidalCategoryStruct.associator Y₃.unmop Y₂.unmop Y₁.unmop).symm.mop.hom).unmop =
    (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator X₃.unmop X₂.unmop X₁.unmop).symm.mop.hom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
            (CategoryTheory.MonoidalCategoryStruct.tensorHom h.unmop g.unmop).mop.unmop f.unmop).mop).unmop