∀ {C₁ : Type u_5} {C₂ : Type u_6} (C₃ : Type u_3) {D₁ : Type u_7} {D₂ : Type u_8} (D₃ : Type u_4)
  [inst : CategoryTheory.Category.{u_13, u_5} C₁] [inst_1 : CategoryTheory.Category.{u_14, u_6} C₂]
  [inst_2 : CategoryTheory.Category.{u_1, u_3} C₃] [inst_3 : CategoryTheory.Category.{u_10, u_7} D₁]
  [inst_4 : CategoryTheory.Category.{u_11, u_8} D₂] [inst_5 : CategoryTheory.Category.{u_2, u_4} D₃] (E : Type u_9)
  [inst_6 : CategoryTheory.Category.{u_12, u_9} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) {X Y Z : CategoryTheory.Functor C₃ D₃} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Functor.whiskeringLeft₃ObjObjMap E F₁ F₂ (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskeringLeft₃ObjObjMap E F₁ F₂ f)
      (CategoryTheory.Functor.whiskeringLeft₃ObjObjMap E F₁ F₂ g)