-- Mathlib/CategoryTheory/Localization/Construction.lean
theorem uniq (G₁ G₂ : W.Localization ⥤ D) (h : W.Q ⋙ G₁ = W.Q ⋙ G₂) : G₁ = G₂

Proof state:
case refine_2.mk.mk.inr.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) ≫ eqToHom ⋯

Tactic:
have hw' := Functor.congr_hom h w

Result:
case refine_2.mk.mk.inr.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : (W.Q ⋙ G₁).map w = eqToHom ⋯ ≫ (W.Q ⋙ G₂).map w ≫ eqToHom ⋯
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) ≫ eqToHom ⋯

Proof state:
case refine_1.h
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X : Paths (LocQuiver W)
⊢ (Quotient.functor (relations W) ⋙ G₁).obj X = (Quotient.functor (relations W) ⋙ G₂).obj X

Tactic:
cases X

Result:
case refine_1.h.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
obj✝ : C
⊢ (Quotient.functor (relations W) ⋙ G₁).obj { obj := obj✝ } = (Quotient.functor (relations W) ⋙ G₂).obj { obj := obj✝ }

Proof state:
case refine_2
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ ∀ (X Y : W.Localization) (f : X ⟶ Y), G₁.map f = eqToHom ⋯ ≫ G₂.map f ≫ eqToHom ⋯

Tactic:
rintro ⟨⟨X⟩⟩ ⟨⟨Y⟩⟩ ⟨f⟩

Result:
case refine_2.mk.mk.mk.mk.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
X Y : C
f✝ : { as := { obj := X } } ⟶ { as := { obj := Y } }
f : { as := { obj := X } }.as ⟶ { as := { obj := Y } }.as
⊢ G₁.map (Quot.mk (Quotient.CompClosure (relations W)) f) =
    eqToHom ⋯ ≫ G₂.map (Quot.mk (Quotient.CompClosure (relations W)) f) ≫ eqToHom ⋯

Proof state:
case refine_2.mk.mk.inr.mk.refine_1
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj Y) = G₂.obj (W.Q.obj Y)

case refine_2.mk.mk.inr.mk.refine_2
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj X) = G₂.obj (W.Q.obj X)

Tactic:
all_goals apply Functor.congr_obj h

Result:
no goals

Proof state:
case refine_2.mk.mk.inr.mk.refine_2
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj X) = G₂.obj (W.Q.obj X)

Tactic:
apply Functor.congr_obj h

Result:
no goals

Proof state:
case refine_2.mk.mk.mk.mk.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
X Y : C
f✝ : { as := { obj := X } } ⟶ { as := { obj := Y } }
f : { as := { obj := X } }.as ⟶ { as := { obj := Y } }.as
⊢ G₁.map (Quot.mk (Quotient.CompClosure (relations W)) f) =
    eqToHom ⋯ ≫ G₂.map (Quot.mk (Quotient.CompClosure (relations W)) f) ≫ eqToHom ⋯

Tactic:
apply Functor.congr_hom h'

Result:
no goals

Proof state:
case refine_2.mk.mk.inl
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
f : { obj := X }.obj ⟶ { obj := Y }.obj
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inl f)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inl f)) ≫ eqToHom ⋯

Tactic:
simpa only using Functor.congr_hom h f

Result:
no goals

Proof state:
case refine_2.mk.mk.inr.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : (W.Q ⋙ G₁).map w = eqToHom ⋯ ≫ (W.Q ⋙ G₂).map w ≫ eqToHom ⋯
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) ≫ eqToHom ⋯

Tactic:
simp only [Functor.comp_map, hw] at hw'

Result:
case refine_2.mk.mk.inr.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) ≫ eqToHom ⋯

Proof state:
case refine_1.h.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
obj✝ : C
⊢ (Quotient.functor (relations W) ⋙ G₁).obj { obj := obj✝ } = (Quotient.functor (relations W) ⋙ G₂).obj { obj := obj✝ }

Tactic:
apply Functor.congr_obj h

Result:
no goals

Proof state:
case refine_2.mk.mk.inr.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw : W w
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw⟩)) ≫ eqToHom ⋯

Tactic:
have hw : W.Q.map w = (wIso w hw).hom := rfl

Result:
case refine_2.mk.mk.inr.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) ≫ eqToHom ⋯