C : Type u
inst✝² : Category C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ ((kernelSubobjectIso f).hom ≫ kernel.ι f) ≫ f = 0
C : Type u
inst✝² : Category C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ arrow (kernelSubobject f) ≫ f = 0
rw [← kernelSubobject_arrow]
no goals
C : Type u
inst✝² : Category C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ ((kernelSubobjectIso f).hom ≫ kernel.ι f) ≫ f = 0
simp only [Category.assoc, kernel.condition, comp_zero]