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