no goals
ι : Type ?u.36234
V : Type u
inst✝⁴ : Category V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝² : HasImage f
g : B ⟶ C
inst✝¹ : HasKernel g
w : f ≫ g = 0
inst✝ : HasCokernel (imageToKernel f g w)
D : V
k : Subobject.underlying.obj (kernelSubobject g) ⟶ D
p : imageToKernel f g w ≫ k = 0
⊢ π f g w ≫ desc f g w k p = k
simp [homology.π, homology.desc]