C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.right)
⊢ Epi (PullbackCone.snd s)
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
⊢ Epi (PullbackCone.snd s)
haveI : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.right) :=
  Abelian.epi_pullback_of_epi_f f g
no goals
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.right)
⊢ Epi (PullbackCone.snd s)
apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)