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