no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ d f ≫ f = 0
simp
no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ π (kernel f) ≫ kernel.ι f ≫ cokernel.π (d f) = 0
rw [← Category.assoc, cokernel.condition]