∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [inst_4 : CategoryTheory.Category.{v_7, u_7} E]
  (F₁ : CategoryTheory.Functor C₁ D₁) {X Y : CategoryTheory.Functor C₂ D₂} (φ : X ⟶ Y)
  (X_1 : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (X_2 : C₁) (c : C₂),
  (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).map φ).app X_1).app X_2).app c =
    (X_1.obj (F₁.obj X_2)).map (φ.app c)