C : Type u
inst✝³ : Category C
X Y Z : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobjectIso 0).hom ≫ image.ι 0 = 0
C : Type u
inst✝³ : Category C
X Y Z : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ arrow (imageSubobject 0) = 0
rw [← imageSubobject_arrow]
no goals
C : Type u
inst✝³ : Category C
X Y Z : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobjectIso 0).hom ≫ image.ι 0 = 0
simp