C : Type u
inst✝¹ : Category C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s
C : Type u
inst✝¹ : Category C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ f ≫ Cofork.π s = 0 ≫ Cofork.π s
rw [← cancel_epi g, ← Category.assoc, ← hh]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s
simp