∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone (F.comp G)) (d : D),
  (CategoryTheory.Functor.Initial.extendCone.obj c).π.app d =
    CategoryTheory.CategoryStruct.comp (c.π.app (CategoryTheory.Functor.Initial.lift F d))
      (G.map (CategoryTheory.Functor.Initial.homToLift F d))