-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean
lemma exists_leftFraction₃ {X Y : C} (f f' f'' : L.obj X ⟶ L.obj Y) :
    ∃ (φ : W.LeftFraction₃ X Y), f = φ.fst.map L (inverts L W) ∧
      f' = φ.snd.map L (inverts L W) ∧
      f'' = φ.thd.map L (inverts L W)

Proof state:
case intro.intro.intro.refine_3
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯
this✝¹ : IsIso (L.map β.s)
this✝ : IsIso (L.map γ.s)
this : IsIso (L.map (β.s ≫ γ.s))
⊢ β.map L ⋯ ≫ L.map β.s ≫ L.map γ.s = ψ.thd.map L ⋯ ≫ L.map (β.s ≫ γ.s)

Tactic:
rw [LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s, L.map_comp]

Result:
no goals

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯

Tactic:
obtain ⟨γ, hγ⟩ := (RightFraction.mk _ α.hs β.s).exists_leftFraction

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : (RightFraction.mk α.s ⋯ β.s).f ≫ γ.s = (RightFraction.mk α.s ⋯ β.s).s ≫ γ.f
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : (RightFraction.mk α.s ⋯ β.s).f ≫ γ.s = (RightFraction.mk α.s ⋯ β.s).s ≫ γ.f
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯

Tactic:
dsimp at hγ

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯

Proof state:
case intro.intro.intro.refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯
this✝¹ : IsIso (L.map β.s)
this✝ : IsIso (L.map γ.s)
this : IsIso (L.map (β.s ≫ γ.s))
⊢ f' = ψ.snd.map L ⋯

Tactic:
rw [← cancel_mono (L.map (β.s ≫ γ.s)), LeftFraction.map_comp_map_s, hα', hγ,
  L.map_comp, LeftFraction.map_comp_map_s_assoc, L.map_comp]

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯

Tactic:
obtain ⟨α, hα, hα'⟩ := exists_leftFraction₂ L W f f'

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯
this : IsIso (L.map β.s)
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯

Tactic:
have := inverts L W _ γ.hs

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯
this✝ : IsIso (L.map β.s)
this : IsIso (L.map γ.s)
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯

Proof state:
case intro.intro.intro.refine_3
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯
this✝¹ : IsIso (L.map β.s)
this✝ : IsIso (L.map γ.s)
this : IsIso (L.map (β.s ≫ γ.s))
⊢ f'' = ψ.thd.map L ⋯

Tactic:
rw [← cancel_mono (L.map (β.s ≫ γ.s)), hβ]

Result:
case intro.intro.intro.refine_3
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯
this✝¹ : IsIso (L.map β.s)
this✝ : IsIso (L.map γ.s)
this : IsIso (L.map (β.s ≫ γ.s))
⊢ β.map L ⋯ ≫ L.map (β.s ≫ γ.s) = ψ.thd.map L ⋯ ≫ L.map (β.s ≫ γ.s)