∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Cᴹᵒᵖ} (x : X₁ ⟶ Y₁) (x_1 : X₂ ⟶ Y₂) (x_2 : Y₁ ⟶ Z₁) (x_3 : Y₂ ⟶ Z₂),
  (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom x_1.unmop x.unmop).mop
        (CategoryTheory.MonoidalCategoryStruct.tensorHom x_3.unmop x_2.unmop).mop).unmop =
    (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp x_1 x_3).unmop
          (CategoryTheory.CategoryStruct.comp x x_2).unmop).mop.unmop