-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : HasBinaryBiproducts.{v₁, u₁} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
rw :
  F.map (CategoryStruct.comp (Y := biprod.{v₁, u₁} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)) = F.map f + F.map g
rw₁ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (F.map (biprod.lift (𝟙 X) (𝟙 X))) (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₂ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (F.map (biprod.desc f g)) =
    F.map f + F.map g
rw₃ :
  CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.inv (F.mapBiprod X X) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj (biprod.{v₁, u₁} X X)))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
        (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) =
    F.map f + F.map g
rw₄ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) : F.obj X ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X X)) (Iso.inv (F.mapBiprod X X))
          (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X))
            (Iso.hom (F.mapBiprod X X) : F.obj (biprod.{v₁, u₁} X X) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj X))
            (biprod.desc (F.map f) (F.map g) : biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y)) :
        biprod.{v₂, u₂} (F.obj X) (F.obj X) ⟶ F.obj Y) =
    F.map f + F.map g
rw₅ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)))
      (biprod.desc (F.map f) (F.map g)) =
    F.map f + F.map g
rw₆ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)))
      (biprod.desc (F.map f) (F.map g)) =
    F.map f + F.map g
rw₇ rw₈ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)))
      (biprod.desc (F.map f) (F.map g)) =
    CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj X)) (biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)))
      (biprod.desc (F.map f) (F.map g))
⊢ F.map (f + g) = F.map f + F.map g

Tactic:
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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.mapBiprod_hom_desc, CategoryTheory.Limits.biprod.lift_mapBiprod, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.biprod.add_eq_lift_id_desc