∀ {J : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} J] {C : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_1, u_4} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (lift : (s : CategoryTheory.Limits.Cone F) → s ⟶ t),
  (∀ (s : CategoryTheory.Limits.Cone F) (m : s ⟶ t), m = lift s) →
    ∀ (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt)
      (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j), { hom := m, w := w } = lift s