∀ (C : Type u_5) [inst : CategoryTheory.Category.{u_6, u_5} C] (D : Type u_3)
  [inst_1 : CategoryTheory.Category.{u_1, u_3} D] (E : Type u_4) [inst_2 : CategoryTheory.Category.{u_2, u_4} E]
  {X Y Z : D ⥤ₑ E} (f : X ⟶ Y) (g : Y ⟶ Z),
  {
      app := fun H =>
        CategoryTheory.ObjectProperty.homMk
          (((CategoryTheory.Functor.whiskeringRight C D E).map (CategoryTheory.CategoryStruct.comp f g).hom).app H.obj),
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      {
        app := fun H =>
          CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map f.hom).app H.obj),
        naturality := ⋯ }
      {
        app := fun H =>
          CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map g.hom).app H.obj),
        naturality := ⋯ }