-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean
lemma map_eq_iff {X Y : C} (φ ψ : W.LeftFraction₂ X Y) :
    (φ.fst.map L (Localization.inverts _ _) = ψ.fst.map L (Localization.inverts _ _) ∧
    φ.snd.map L (Localization.inverts _ _) = ψ.snd.map L (Localization.inverts _ _)) ↔
      LeftFraction₂Rel φ ψ

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
⊢ LeftFraction₂Rel φ ψ

Tactic:
obtain ⟨Z''', u', hu', fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ ψ.hs hα'

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac' : (t₂ ≫ α.f ≫ u) ≫ u' = (t₂' ≫ α.s ≫ u) ≫ u'
⊢ LeftFraction₂Rel φ ψ

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : (RightFraction.mk (φ.s ≫ t₁) ht (φ.s ≫ t₁')).f ≫ α.s = (RightFraction.mk (φ.s ≫ t₁) ht (φ.s ≫ t₁')).s ≫ α.f
⊢ LeftFraction₂Rel φ ψ

Tactic:
simp only [Category.assoc] at hα

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

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
⊢ ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u

Tactic:
rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
⊢ φ.fst.map L ⋯ = ψ.fst.map L ⋯ ∧ φ.snd.map L ⋯ = ψ.snd.map L ⋯ ↔ LeftFraction₂Rel φ ψ

Tactic:
simp only [LeftFraction.map_eq_iff L W]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
⊢ LeftFractionRel φ.fst ψ.fst ∧ LeftFractionRel φ.snd ψ.snd ↔ LeftFraction₂Rel φ ψ

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
⊢ LeftFraction₂Rel φ ψ

Tactic:
have hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u := by
  rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
⊢ LeftFraction₂Rel φ ψ

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
h : LeftFractionRel φ.fst ψ.fst
h' : LeftFractionRel φ.snd ψ.snd
⊢ LeftFraction₂Rel φ ψ

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h

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