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