no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : HasImage g
h : f ≫ g = 0
⊢ (f ≫ factorThruImage g) ≫ image.ι g = 0
simp [h]