Lean4
/-- The second leg of a pushout cocone is a regular epimorphism if the right component is too.
See also `Pushout.sndOfEpi` for the basic epimorphism version, and
`regularOfIsPushoutFstOfRegular` for the flipped version.
-/
def regularOfIsPushoutSndOfRegular {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [gr : RegularEpi g]
(comm : f ≫ h = g ≫ k) (t : IsColimit (PushoutCocone.mk _ _ comm)) : RegularEpi h
where
W := gr.W
left := gr.left ≫ f
right := gr.right ≫ f
w := by rw [Category.assoc, Category.assoc, comm]; simp only [← Category.assoc, eq_whisker gr.w]
isColimit := by
apply Cofork.IsColimit.mk' _ _
intro s
have l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π := by rw [← Category.assoc, ← Category.assoc, s.condition]
obtain ⟨l, hl⟩ := Cofork.IsColimit.desc' gr.isColimit (f ≫ Cofork.π s) l₁
obtain ⟨p, hp₁, _⟩ := PushoutCocone.IsColimit.desc' t _ _ hl.symm
refine ⟨p, hp₁, ?_⟩
intro m w
have z := w.trans hp₁.symm
apply t.hom_ext
apply (PushoutCocone.mk _ _ comm).coequalizer_ext
· exact z
· erw [← cancel_epi g, ← Category.assoc, ← eq_whisker comm]
erw [← Category.assoc, ← eq_whisker comm]
dsimp at z; simp only [Category.assoc, z]
