no goals
C : Type u
inst✝⁶ : Category C
D : Type u
inst✝⁵ : Category D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : PreservesFiniteLimits F
inst✝ : Mono f
ex : Exact f g
⊢ F.map f ≫ F.map g = 0
simp [← Functor.map_comp, ex.w]