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 = arrow (kernelSubobject f)
simp [kernelSubobjectIso]