-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma uniq (F₁ F₂ : Localization W ⥤ E) (h : Q W ⋙ F₁ = Q W ⋙ F₂) : F₁ = F₂ :=
  Functor.ext (fun X => Functor.congr_obj h X) (by
    rintro (X Y : C) f
    obtain ⟨f, rfl⟩ := Hom.mk_surjective f
    rw [show Hom.mk f = homMk (mk f.f f.s f.hs) by rfl,
      ← Q_map_comp_Qinv f.f f.s f.hs, F₁.map_comp, F₂.map_comp, assoc]
    erw [Functor.congr_hom h f.f]
    rw [assoc, assoc]
    congr 2
    have := inverts W _ f.hs
    rw [← cancel_epi (F₂.map ((Q W).map f.s)), ← F₂.map_comp_assoc,
      Qiso_hom_inv_id, Functor.map_id, id_comp]
    erw [Functor.congr_hom h.symm f.s]
    dsimp
    rw [assoc, assoc, eqToHom_trans_assoc, eqToHom_refl, id_comp, ← F₁.map_comp,
      Qiso_hom_inv_id]
    dsimp
    rw [F₁.map_id, comp_id])

Proof state:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
⊢ ∀ (X Y : Localization W) (f : X ⟶ Y), F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯

Tactic:
rintro (X Y : C) f

Result:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : X ⟶ Y
⊢ F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯

Proof state:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₁).map f.s ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯

Tactic:
dsimp

Result:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ (eqToHom ⋯ ≫ F₁.map ((Q W).map f.s) ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯

Proof state:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ F₂.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯

Tactic:
erw [Functor.congr_hom h.symm f.s]

Result:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₁).map f.s ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯

Proof state:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : X ⟶ Y
⊢ F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯

Tactic:
obtain ⟨f, rfl⟩ := Hom.mk_surjective f

Result:
case intro
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ F₁.map (Hom.mk f) = eqToHom ⋯ ≫ F₂.map (Hom.mk f) ≫ eqToHom ⋯

Proof state:
case intro
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₂).map f.f ≫ eqToHom ⋯) ≫ F₁.map (Qinv f.s ⋯) =
    eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
rw [assoc, assoc]

Result:
case intro
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ eqToHom ⋯ ≫ (Q W ⋙ F₂).map f.f ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) =
    eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Proof state:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 ((Q W).obj Y)) = eqToHom ⋯

Tactic:
dsimp

Result:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 Y) = eqToHom ⋯

Proof state:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
rw [← cancel_epi (F₂.map ((Q W).map f.s)), ← F₂.map_comp_assoc,
  Qiso_hom_inv_id, Functor.map_id, id_comp]

Result:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ F₂.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯

Proof state:
case intro
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ eqToHom ⋯ ≫ (Q W ⋙ F₂).map f.f ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) =
    eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
congr 2

Result:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Proof state:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
have := inverts W _ f.hs

Result:
case intro.e_a.e_a
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Proof state:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ Hom.mk f = homMk (mk f.f f.s ⋯)

Tactic:
rfl

Result:
no goals