Creation of limits and pullbacks

We show some lemmas relating creation of (co)limits and pullbacks (resp. pushouts).

theorem CategoryTheory.Limits.HasPullback.of_createsLimit {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (F : Functor C D) {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CreatesLimit (cospan f g) F] [HasPullback (F.map f) (F.map g)] : HasPullback f g

theorem CategoryTheory.Limits.HasPushout.of_createsColimit {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (F : Functor C D) {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [CreatesColimit (span f g) F] [HasPushout (F.map f) (F.map g)] : HasPushout f g