∀ {C₁ : Type u_5} {C₂ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_4} [inst : CategoryTheory.Category.{u_10, u_5} C₁]
  [inst_1 : CategoryTheory.Category.{u_1, u_3} C₂] [inst_2 : CategoryTheory.Category.{u_8, u_6} D₁]
  [inst_3 : CategoryTheory.Category.{u_2, u_4} D₂] (E : Type u_7) [inst_4 : CategoryTheory.Category.{u_9, u_7} E]
  {X Y : CategoryTheory.Functor C₁ D₁} (ψ : X ⟶ Y) ⦃X_1 Y_1 : CategoryTheory.Functor C₂ D₂⦄ (f : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ({
            obj := fun F₂ =>
              ((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ E)
                        (CategoryTheory.Functor C₂ E)).obj
                    ((CategoryTheory.Functor.whiskeringLeft C₂ D₂ E).obj F₂)).comp
                ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ E)).obj X),
            map := fun {X_2 Y} φ =>
              CategoryTheory.Functor.whiskerRight
                ((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ E)
                      (CategoryTheory.Functor C₂ E)).map
                  ((CategoryTheory.Functor.whiskeringLeft C₂ D₂ E).map φ))
                ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ E)).obj X),
            map_id := ⋯, map_comp := ⋯ }.map
        f)
      (((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ E) (CategoryTheory.Functor C₂ E)).obj
            ((CategoryTheory.Functor.whiskeringLeft C₂ D₂ E).obj Y_1)).whiskerLeft
        ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ E)).map ψ)) =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ E) (CategoryTheory.Functor C₂ E)).obj
            ((CategoryTheory.Functor.whiskeringLeft C₂ D₂ E).obj X_1)).whiskerLeft
        ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ E)).map ψ))
      ({
            obj := fun F₂ =>
              ((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ E)
                        (CategoryTheory.Functor C₂ E)).obj
                    ((CategoryTheory.Functor.whiskeringLeft C₂ D₂ E).obj F₂)).comp
                ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ E)).obj Y),
            map := fun {X Y_2} φ =>
              CategoryTheory.Functor.whiskerRight
                ((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ E)
                      (CategoryTheory.Functor C₂ E)).map
                  ((CategoryTheory.Functor.whiskeringLeft C₂ D₂ E).map φ))
                ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ E)).obj Y),
            map_id := ⋯, map_comp := ⋯ }.map
        f)