C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y : C
⊢ F.map 0 = 0
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y : C
f : X ⟶ Y
⊢ f = 0 → F.map f = 0
rintro rfl
no goals
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y : C
⊢ F.map 0 = 0
exact F.map_zero _ _