C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
X Y : C
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
h : f = 0
⊢ IsZero X
subst h
no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ IsZero X
apply of_mono_zero X Y