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