∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C}
  {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s)
  {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t),
  CategoryTheory.CategoryStruct.comp t.fst
      (Q.lift
        (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.id X)
          (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }))) =
    CategoryTheory.CategoryStruct.id t.pt