∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} (f : F ⟶ H) (g : G ⟶ H)
  (c : (X : D) → CategoryTheory.Limits.PullbackCone (f.app X) (g.app X))
  (hc : (X : D) → CategoryTheory.Limits.IsLimit (c X)) (X : D),
  (CategoryTheory.Limits.PullbackCone.combine f g c hc).pt.obj X = (c X).pt