-- 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
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
have eq := this ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv)
  ((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)

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 ≫ 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

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 ≫ 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

Tactic:
rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
  ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]

Result:
no goals

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
a✝ : G.Additive
⊢ (L ⋙ G).Additive

Tactic:
infer_instance

Result:
no goals

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
⊢ G.map (φ.fst.map L ⋯ + φ.snd.map L ⋯) = G.map (φ.fst.map L ⋯) + G.map (φ.snd.map L ⋯)

Tactic:
have := Localization.inverts L W φ.s φ.hs

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
this : IsIso (L.map φ.s)
⊢ G.map (φ.fst.map L ⋯ + φ.snd.map L ⋯) = G.map (φ.fst.map L ⋯) + G.map (φ.snd.map L ⋯)

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:
intros X Y f g

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:
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
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
have hL := essSurj L W

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
⊢ G.map (f + g) = G.map f + G.map g

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
⊢ G.Additive

Tactic:
refine ⟨fun {X Y f g} => ?_⟩

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
⊢ G.map (f + g) = G.map f + G.map g