-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
lemma add'_eq (f₁ f₂ : L.obj X ⟶ L.obj Y) (φ : W.LeftFraction₂ X Y)
    (hφ₁ : f₁ = φ.fst.map L (inverts L W))
    (hφ₂ : f₂ = φ.snd.map L (inverts L W)) :
    add' W f₁ f₂ = φ.add.map L (inverts L W)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
⊢ add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯

Tactic:
have := inverts L W _ ht

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯

Proof state:
case intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
⊢ add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, hft', ht⟩ := (LeftFraction₂.map_eq_iff L W φ₀ φ).1 ⟨hφ₁, hφ₂⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
⊢ add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ φ₀.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁) = φ.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)

Tactic:
nth_rw 2 [hst]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ φ₀.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁) = φ.add.map L ⋯ ≫ L.map (φ.s ≫ t₂)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ φ₀.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁) = φ.add.map L ⋯ ≫ L.map (φ.s ≫ t₂)

Tactic:
rw [L.map_comp, L.map_comp, LeftFraction.map_comp_map_s_assoc,
  LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ← L.map_comp,
  add_comp, add_comp, hft, hft']

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : L.obj X ⟶ L.obj Y
φ : W.LeftFraction₂ X Y
hφ₁ : f₁ = φ.fst.map L ⋯
hφ₂ : f₂ = φ.snd.map L ⋯
⊢ add' W f₁ f₂ = φ.add.map L ⋯

Tactic:
obtain ⟨φ₀, rfl, rfl, hφ₀⟩ : ∃ (φ₀ : W.LeftFraction₂ X Y)
  (_ : f₁ = φ₀.fst.map L (inverts L W))
  (_ : f₂ = φ₀.snd.map L (inverts L W)),
  add' W f₁ f₂ = φ₀.add.map L (inverts L W) :=
  ⟨(exists_leftFraction₂ L W f₁ f₂).choose,
    (exists_leftFraction₂ L W f₁ f₂).choose_spec.1,
    (exists_leftFraction₂ L W f₁ f₂).choose_spec.2, rfl⟩

Result:
case intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
⊢ add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯

Tactic:
rw [hφ₀, ← cancel_mono (L.map (φ₀.s ≫ t₁))]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ φ₀.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁) = φ.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)