∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_4, u_1} C] (D : Type u_6)
  [inst_1 : CategoryTheory.Category.{u_5, u_6} D] (E : Type u_3) [inst_2 : CategoryTheory.Category.{u_2, u_3} E]
  {X Y : CategoryTheory.Functor D E} (τ : X ⟶ Y) (X_1 Y_1 : CategoryTheory.Functor C D) (f : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun F => F.comp X, map := fun {X_2 Y} α => CategoryTheory.Functor.whiskerRight α X, map_id := ⋯,
            map_comp := ⋯ }.map
        f)
      { app := fun c => τ.app (Y_1.obj c), naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp { app := fun c => τ.app (X_1.obj c), naturality := ⋯ }
      ({ obj := fun F => F.comp Y, map := fun {X Y_2} α => CategoryTheory.Functor.whiskerRight α Y, map_id := ⋯,
            map_comp := ⋯ }.map
        f)