no goals
C : Type u
inst✝² : Category C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : Factors (kernelSubobject f) h
⊢ h ≫ f = 0
rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp,
  comp_zero]