∀ {C : Type u_7} [inst : CategoryTheory.Category.{u_8, u_7} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u_6}
  [inst_3 : CategoryTheory.Category.{u_5, u_6} E] {G : CategoryTheory.Functor D E} {B : Type u_2}
  [inst_4 : CategoryTheory.Category.{u_1, u_2} B] {H : CategoryTheory.Functor E B}
  [inst_5 : CategoryTheory.CreatesLimit (F.comp G) H] {c : CategoryTheory.Limits.Cone (G.comp H)}
  (hc : CategoryTheory.Limits.IsLimit c) (j : D),
  (H.mapCone
            (CategoryTheory.Functor.Initial.extendCone.obj
              (CategoryTheory.liftLimit ((CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F c).symm hc)))).π.app
      j =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          (H.mapCone
              (CategoryTheory.Functor.Initial.extendCone.obj
                (CategoryTheory.liftLimit ((CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F c).symm hc)))).pt).hom
      ((CategoryTheory.Functor.Initial.extendCone.obj
              (H.mapCone
                (CategoryTheory.liftLimit ((CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F c).symm hc)))).π.app
        j)