-- Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
lemma additive_of_full_essSurj_comp [Full F] [EssSurj F] (G : D ⥤ E)
    [(F ⋙ G).Additive] : G.Additive where
  map_add {X Y f g}

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = (F ⋙ G).map (f' + g')

Tactic:
dsimp

Result:
case intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = G.map (F.map (f' + g'))

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = G.map (F.map (f' + g'))

Tactic:
rw [F.map_add]

Result:
no goals

Proof state:
case intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
obtain ⟨g', hg'⟩ := F.map_surjective ((F.objObjPreimageIso X).hom ≫ g ≫
  (F.objObjPreimageIso Y).inv)

Result:
case intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map
      ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv +
        (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv) =
    G.map ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) +
      G.map ((F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv)

Tactic:
erw [← hf', ← hg', ← (F ⋙ G).map_add]

Result:
case intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = (F ⋙ G).map (f' + g')

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
obtain ⟨f', hf'⟩ := F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫
  (F.objObjPreimageIso Y).inv)

Result:
case intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
simp only [← cancel_mono (G.map (F.objObjPreimageIso Y).inv),
  ← cancel_epi (G.map (F.objObjPreimageIso X).hom),
  Preadditive.add_comp, Preadditive.comp_add, ← Functor.map_comp]

Result:
case intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : Category.{u_6, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map
      ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv +
        (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv) =
    G.map ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) +
      G.map ((F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv)