C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
hf : f = 0
⊢ IsZero X
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
⊢ IsZero X
have hf := i.eq_zero_of_tgt f
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
X Y : C
i : IsZero Y
inst✝ : Mono 0
⊢ IsZero X
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
hf : f = 0
⊢ IsZero X
subst hf
no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
X Y : C
i : IsZero Y
inst✝ : Mono 0
⊢ IsZero X
exact IsZero.of_mono_zero X Y