-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_5 : Category.{v_3, u_3} E
inst_6 : Preadditive.{v_3, u_3} E
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : L.Additive
G : Functor.{v_2, v_3, u_2, u_3} D E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
mpr :
  G.map (φ.add (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
mpr₁ :
  G.map (φ.add (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₂ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₃ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₄ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₅ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₆ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₇ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₈ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
mpr₉ :
  (L ⋙ G).map (φ.add (W := W).f (W := W)) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
mpr₁₀ :
  (L ⋙ G).map (φ.f (W := W)) + (L ⋙ G).map (φ.f' (W := W)) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
mpr₁₁ :
  G.map (L.map (φ.f (W := W))) + (L ⋙ G).map (φ.f' (W := W)) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
mpr₁₂ mpr₁₃ :
  G.map (L.map (φ.f (W := W))) + G.map (L.map (φ.f' (W := W))) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
⊢ G.map (φ.fst (W := W).map (W := W) L ⋯ + φ.snd (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) 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]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.map_add, CategoryTheory.MorphismProperty.LeftFraction₂.s, CategoryTheory.Functor.map_add, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Preadditive.add_comp, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.Localization.inverts, CategoryTheory.Functor.comp_map