no goals
C : Type u
inst✝⁴ : Category C
inst✝³ : Abelian C
inst✝² : HasPushouts C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
g₁ : X ⟶ W
inst✝¹ : Epi g₁
g₂ : W ⟶ Z
inst✝ : Mono g₂
hg : g₁ ≫ g₂ = g
f' : W ⟶ Y
hf : g₁ ≫ f' = f
t : PushoutCocone f g
ht : IsColimit t
⊢ Mono (PushoutCocone.inl t)
apply mono_inl_of_isColimit _ _ (PushoutCocone.isColimitOfFactors _ _ _ _ _ hf hg t ht)