feat: functor creates limit if it lifts a single limit cone (#11482)

Author: TwoFX

Mathlib/CategoryTheory/Limits/Creates.lean

@@ -278,6 +278,16 @@ def createsLimitOfReflectsIso {K : J ⥤ C} {F : C ⥤ D} [ReflectsIsomorphisms
         exact IsLimit.ofIsoLimit hd' (asIso f).symm }
 #align category_theory.creates_limit_of_reflects_iso CategoryTheory.createsLimitOfReflectsIso
 
+/-- If `F` reflects isomorphisms and we can lift a single limit cone to a limit cone, then `F`
+    creates limits. Note that unlike `createsLimitOfReflectsIso`, to apply this result it is
+    necessary to know that `K ⋙ F` actually has a limit. -/
+def createsLimitOfReflectsIso' {K : J ⥤ C} {F : C ⥤ D} [ReflectsIsomorphisms F]
+    {c : Cone (K ⋙ F)} (hc : IsLimit c) (h : LiftsToLimit K F c hc) : CreatesLimit K F :=
+  createsLimitOfReflectsIso fun _ t =>
+    { liftedCone := h.liftedCone
+      validLift := h.validLift ≪≫ IsLimit.uniqueUpToIso hc t
+      makesLimit := h.makesLimit }
+
 -- Notice however that even if the isomorphism is `Iso.refl _`,
 -- this construction will insert additional identity morphisms in the cone maps,
 -- so the constructed limits may not be ideal, definitionally.
@@ -390,6 +400,16 @@ def createsColimitOfReflectsIso {K : J ⥤ C} {F : C ⥤ D} [ReflectsIsomorphism
         exact IsColimit.ofIsoColimit hd' (asIso f) }
 #align category_theory.creates_colimit_of_reflects_iso CategoryTheory.createsColimitOfReflectsIso
 
+/-- If `F` reflects isomorphisms and we can lift a single colimit cocone to a colimit cocone, then
+    `F` creates limits. Note that unlike `createsColimitOfReflectsIso`, to apply this result it is
+    necessary to know that `K ⋙ F` actually has a colimit. -/
+def createsColimitOfReflectsIso' {K : J ⥤ C} {F : C ⥤ D} [ReflectsIsomorphisms F]
+    {c : Cocone (K ⋙ F)} (hc : IsColimit c) (h : LiftsToColimit K F c hc) : CreatesColimit K F :=
+  createsColimitOfReflectsIso fun _ t =>
+    { liftedCocone := h.liftedCocone
+      validLift := h.validLift ≪≫ IsColimit.uniqueUpToIso hc t
+      makesColimit := h.makesColimit }
+
 -- Notice however that even if the isomorphism is `Iso.refl _`,
 -- this construction will insert additional identity morphisms in the cocone maps,
 -- so the constructed colimits may not be ideal, definitionally.