∀ {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 Y Z : CategoryTheory.Functor C D} (f : X ⟶ Y) (g : Y ⟶ Z),
  {
      app := fun X₁ =>
        {
          app := fun X₂ =>
            CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.CategoryStruct.comp f g).app X₁)
              ((CategoryTheory.CategoryStruct.comp f g).app X₂),
          naturality := ⋯ },
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      {
        app := fun X₁ =>
          { app := fun X₂ => CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app X₁) (f.app X₂), naturality := ⋯ },
        naturality := ⋯ }
      {
        app := fun X₁ =>
          { app := fun X₂ => CategoryTheory.MonoidalCategoryStruct.tensorHom (g.app X₁) (g.app X₂), naturality := ⋯ },
        naturality := ⋯ }