{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : C} →
        {Y : ι → C} →
          {f : (i : ι) → Y i ⟶ X} →
            (s : CategoryTheory.Limits.WidePullbackCone f) →
              (lift : (t : CategoryTheory.Limits.WidePullbackCone f) → t.pt ⟶ s.pt) →
                (∀ (t : CategoryTheory.Limits.WidePullbackCone f),
                    CategoryTheory.CategoryStruct.comp (lift t) s.base = t.base) →
                  (∀ (t : CategoryTheory.Limits.WidePullbackCone f) (i : ι),
                      CategoryTheory.CategoryStruct.comp (lift t) (s.π i) = t.π i) →
                    (∀ (t : CategoryTheory.Limits.WidePullbackCone f) (m : t.pt ⟶ s.pt),
                        CategoryTheory.CategoryStruct.comp m s.base = t.base →
                          (∀ (i : ι), CategoryTheory.CategoryStruct.comp m (s.π i) = t.π i) → m = lift t) →
                      CategoryTheory.Limits.IsLimit s