no goals
C : Type u₁
D : Type u₂
inst✝⁶ : Category C
inst✝⁵ : Category D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryBiproducts C
inst✝¹ : PreservesZeroMorphisms F
inst✝ : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ F.map (f + g) = F.map f + F.map g
rw [biprod.add_eq_lift_id_desc,  F.map_comp, ← biprod.lift_mapBiprod,
  ←  biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
  biprod.add_eq_lift_id_desc]