∀ (C : Type u_3) [inst : CategoryTheory.Category.{u_1, u_3} C] (D : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] (E : Type u_6) [inst_2 : CategoryTheory.Category.{u_5, u_6} E]
  {F G : D ⥤ₗ E} (η : F ⟶ G) ⦃X Y : C ⥤ₗ D⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.leftExactFunctor C E).lift
            ((CategoryTheory.LeftExactFunctor.forget C D).comp
              ((CategoryTheory.Functor.whiskeringRight C D E).obj F.obj))
            ⋯).map
        f)
      (CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app Y.obj)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app X.obj))
      (((CategoryTheory.leftExactFunctor C E).lift
            ((CategoryTheory.LeftExactFunctor.forget C D).comp
              ((CategoryTheory.Functor.whiskeringRight C D E).obj G.obj))
            ⋯).map
        f)