∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.Functor C D} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
      (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃))