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

Proof state:
case 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φ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ neg' W (φ₀.map L ⋯) ≫ L.map (φ₀.s ≫ t₁) = φ.neg.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)

Tactic:
nth_rw 1 [L.map_comp]

Result:
case 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φ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ neg' W (φ₀.map L ⋯) ≫ L.map φ₀.s ≫ L.map t₁ = φ.neg.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)

Proof state:
case 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φ : LeftFractionRel φ₀ φ
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯

Tactic:
obtain ⟨Y', t₁, t₂, hst, hft, ht⟩ := hφ

Result:
case 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φ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯

Proof state:
case 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φ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯

Tactic:
have := inverts L W _ ht

Result:
case 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φ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯

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 : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
⊢ neg' W f = φ.neg.map L ⋯

Tactic:
obtain ⟨φ₀, rfl, hφ₀⟩ : ∃ (φ₀ : W.LeftFraction X Y)
  (_ : f = φ₀.map L (inverts L W)),
    neg' W f = φ₀.neg.map L (inverts L W) :=
  ⟨_, (exists_leftFraction L W f).choose_spec, rfl⟩

Result:
case 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φ : φ₀.map L ⋯ = φ.map L ⋯
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯

Proof state:
case 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φ : φ₀.map L ⋯ = φ.map L ⋯
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯

Tactic:
rw [MorphismProperty.LeftFraction.map_eq_iff] at hφ

Result:
case 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φ : LeftFractionRel φ₀ φ
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯

Proof state:
case 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φ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ neg' W (φ₀.map L ⋯) ≫ L.map φ₀.s ≫ L.map t₁ = φ.neg.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)

Tactic:
rw [hφ₀, hst, LeftFraction.map_comp_map_s_assoc, L.map_comp,
  LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ← L.map_comp,
  neg_comp, neg_comp, hft]

Result:
no goals

Proof state:
case 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φ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯

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

Result:
case 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φ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ neg' W (φ₀.map L ⋯) ≫ L.map (φ₀.s ≫ t₁) = φ.neg.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)