∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} 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.unop x_1.unop).op
      (CategoryTheory.MonoidalCategoryStruct.tensorHom x_2.unop x_3.unop).op =
    (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp x x_2).unop
        (CategoryTheory.CategoryStruct.comp x_1 x_3).unop).op