-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
lemma functor_additive_iff {E : Type*} [Category E] [Preadditive E] [Preadditive D] [L.Additive]
    (G : D ⥤ E) :
    G.Additive ↔ (L ⋙ G).Additive

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map
      ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv +
        (L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv) =
    G.map ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv) +
      G.map ((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp,
  ← comp_add, ← comp_add, ← add_comp, ← add_comp, Functor.map_comp, Functor.map_comp] at eq

Result:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map (L.objObjPreimageIso X).hom ≫ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
⊢ G.Additive

Tactic:
suffices ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g by
  refine ⟨fun {X Y f g} => ?_⟩
  have hL := essSurj L W
  have eq := this ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv)
    ((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)
  rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp,
    ← comp_add, ← comp_add, ← add_comp, ← add_comp, Functor.map_comp, Functor.map_comp] at eq
  rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
    ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
⊢ ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ (L ⋙ G).Additive → G.Additive

Tactic:
intro h

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
⊢ G.Additive

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ G.Additive ↔ (L ⋙ G).Additive

Tactic:
constructor

Result:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ G.Additive → (L ⋙ G).Additive

case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ (L ⋙ G).Additive → G.Additive

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ G.Additive → (L ⋙ G).Additive

Tactic:
intro

Result:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
a✝ : G.Additive
⊢ (L ⋙ G).Additive

Proof state:
case mpr.intro.intro
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
this : IsIso (L.map φ.s)
⊢ G.map (φ.fst.map L ⋯ + φ.snd.map L ⋯) = G.map (φ.fst.map L ⋯) + G.map (φ.snd.map L ⋯)

Tactic:
rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp,
  add_comp, ← G.map_comp, ← G.map_comp, LeftFraction.map_comp_map_s,
  LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ← Functor.comp_map,
  Functor.map_add, Functor.comp_map, Functor.comp_map]

Result:
no goals

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
f g : L.obj X ⟶ L.obj Y
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
obtain ⟨φ, rfl, rfl⟩ := exists_leftFraction₂ L W f g

Result:
case mpr.intro.intro
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{u_4, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
⊢ G.map (φ.fst.map L ⋯ + φ.snd.map L ⋯) = G.map (φ.fst.map L ⋯) + G.map (φ.snd.map L ⋯)