chore(CategoryTheory): add IsRegularEpi.of_epi_of_exists and IsRegularEpi.exists_of_isKernelPair (#35862)

From Proetale.

Author: chrisflav

Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean

@@ -229,4 +229,9 @@ theorem of_hasPullback (f : X ⟶ Y) [HasPullback f f] :
 
 end IsKernelPair
 
+lemma IsRegularEpi.exists_of_isKernelPair {X Y : C} (π : X ⟶ Y) [IsRegularEpi π] {Z : C}
+    {fst snd : Z ⟶ X} (h : IsKernelPair π fst snd) {W : C} (f : X ⟶ W) (w : fst ≫ f = snd ≫ f) :
+    ∃ (g : Y ⟶ W), π ≫ g = f :=
+  ⟨h.toCoequalizer'.desc (Cofork.ofπ f w), Cofork.IsColimit.π_desc h.toCoequalizer'⟩
+
 end CategoryTheory

Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

@@ -449,6 +449,15 @@ def regularEpiOfKernelPair {B X : C} (f : X ⟶ B) [HasPullback f f]
   w := pullback.condition
   isColimit := hc
 
+lemma IsRegularEpi.of_epi_of_exists {X B : C} {f : X ⟶ B} [HasPullback f f] [Epi f]
+    (h : ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄, pullback.fst f f ≫ g = pullback.snd f f ≫ g →
+      ∃ (u : B ⟶ Z), f ≫ u = g) :
+    IsRegularEpi f := by
+  refine ⟨⟨regularEpiOfKernelPair _ <| Cofork.IsColimit.mk' _ fun s ↦ ?_⟩⟩
+  choose g hg using h s.condition
+  refine ⟨g, hg, fun hm ↦ ?_⟩
+  rwa [← cancel_epi f, hg]
+
 /-- The data of an `EffectiveEpi` structure on a `RegularEpi`. -/
 def effectiveEpiStructOfRegularEpi {B X : C} {f : X ⟶ B} (hf : RegularEpi f) :
     EffectiveEpiStruct f where