∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsRegularEpi f] (k : X ⟶ Z)
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.left f) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.right f) k),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsRegularEpi.desc f k h) = k