C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ G₁ = G₂

case h'
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
⊢ Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
⊢ G₁ = G₂
suffices h' : Quotient.functor _ ⋙ G₁ = Quotient.functor _ ⋙ G₂
case refine'_1
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ ∀ (X : MorphismProperty.Localization W), G₁.obj X = G₂.obj X

case refine'_2
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ ∀ (X Y : MorphismProperty.Localization W) (f : X ⟶ Y),
    G₁.map f = eqToHom (_ : ?m.26212.obj X = ?m.26213.obj X) ≫ G₂.map f ≫ eqToHom (_ : G₂.obj Y = G₁.obj Y)
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ G₁ = G₂
refine' Functor.ext _ _
case refine'_1.mk.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
X : C
⊢ G₁.obj { as := { obj := X } } = G₂.obj { as := { obj := X } }
case refine'_1
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ ∀ (X : MorphismProperty.Localization W), G₁.obj X = G₂.obj X
rintro ⟨⟨X⟩⟩
no goals
case refine'_1.mk.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
X : C
⊢ G₁.obj { as := { obj := X } } = G₂.obj { as := { obj := X } }
apply Functor.congr_obj h
case refine'_2.mk.mk.mk.mk.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ 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₁.obj { as := { obj := X } } = G₂.obj { as := { obj := X } }) ≫
      G₂.map (Quot.mk (Quotient.CompClosure (relations W)) f) ≫
        eqToHom (_ : G₂.obj { as := { obj := Y } } = G₁.obj { as := { obj := Y } })
case refine'_2
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ ∀ (X Y : MorphismProperty.Localization W) (f : X ⟶ Y),
    G₁.map f = eqToHom (_ : G₁.obj X = G₂.obj X) ≫ G₂.map f ≫ eqToHom (_ : G₂.obj Y = G₁.obj Y)
rintro ⟨⟨X⟩⟩ ⟨⟨Y⟩⟩ ⟨f⟩
no goals
case refine'_2.mk.mk.mk.mk.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ 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₁.obj { as := { obj := X } } = G₂.obj { as := { obj := X } }) ≫
      G₂.map (Quot.mk (Quotient.CompClosure (relations W)) f) ≫
        eqToHom (_ : G₂.obj { as := { obj := Y } } = G₁.obj { as := { obj := Y } })
apply Functor.congr_hom h'
case h'.refine'_1
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
⊢ (Quotient.functor (relations W) ⋙ G₁).toPrefunctor.obj = (Quotient.functor (relations W) ⋙ G₂).toPrefunctor.obj

case h'.refine'_2
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
⊢ ∀ (a b : LocQuiver W) (e : a ⟶ b),
    (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath e) =
      eqToHom (_ : (Quotient.functor (relations W) ⋙ G₁).obj a = (Quotient.functor (relations W) ⋙ G₂).obj a) ≫
        (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath e) ≫
          eqToHom (_ : (Quotient.functor (relations W) ⋙ G₂).obj b = (Quotient.functor (relations W) ⋙ G₁).obj b)
case h'
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
⊢ Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
refine' Paths.ext_functor _ _
case h'.refine'_1.h
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X : Paths (LocQuiver W)
⊢ (Quotient.functor (relations W) ⋙ G₁).obj X = (Quotient.functor (relations W) ⋙ G₂).obj X
case h'.refine'_1
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
⊢ (Quotient.functor (relations W) ⋙ G₁).toPrefunctor.obj = (Quotient.functor (relations W) ⋙ G₂).toPrefunctor.obj
ext X
case h'.refine'_1.h.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
obj✝ : C
⊢ (Quotient.functor (relations W) ⋙ G₁).obj { obj := obj✝ } = (Quotient.functor (relations W) ⋙ G₂).obj { obj := obj✝ }
case h'.refine'_1.h
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X : Paths (LocQuiver W)
⊢ (Quotient.functor (relations W) ⋙ G₁).obj X = (Quotient.functor (relations W) ⋙ G₂).obj X
cases X
no goals
case h'.refine'_1.h.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
obj✝ : C
⊢ (Quotient.functor (relations W) ⋙ G₁).obj { obj := obj✝ } = (Quotient.functor (relations W) ⋙ G₂).obj { obj := obj✝ }
apply Functor.congr_obj h
case h'.refine'_2.mk.mk.inl
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ 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₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inl f)) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })

case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ 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 { val := w, property := hw })) =
    eqToHom
        (_ :
          (Quotient.functor (relations W) ⋙ G₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw })) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })
case h'.refine'_2
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
⊢ ∀ (a b : LocQuiver W) (e : a ⟶ b),
    (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath e) =
      eqToHom (_ : (Quotient.functor (relations W) ⋙ G₁).obj a = (Quotient.functor (relations W) ⋙ G₂).obj a) ≫
        (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath e) ≫
          eqToHom (_ : (Quotient.functor (relations W) ⋙ G₂).obj b = (Quotient.functor (relations W) ⋙ G₁).obj b)
rintro ⟨X⟩ ⟨Y⟩ (f | ⟨w, hw⟩)
no goals
case h'.refine'_2.mk.mk.inl
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ 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₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inl f)) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })
simpa only using Functor.congr_hom h f
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) =
    eqToHom
        (_ :
          (Quotient.functor (relations W) ⋙ G₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ 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 { val := w, property := hw })) =
    eqToHom
        (_ :
          (Quotient.functor (relations W) ⋙ G₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw })) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })
have hw : W.Q.map w = (wIso w hw).hom := rfl
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
hw' :
  (MorphismProperty.Q W ⋙ G₁).map w =
    eqToHom (_ : (MorphismProperty.Q W ⋙ G₁).obj { obj := Y }.obj = (MorphismProperty.Q W ⋙ G₂).obj { obj := Y }.obj) ≫
      (MorphismProperty.Q W ⋙ G₂).map w ≫
        eqToHom
          (_ : (MorphismProperty.Q W ⋙ G₂).obj { obj := X }.obj = (MorphismProperty.Q W ⋙ G₁).obj { obj := X }.obj)
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) =
    eqToHom
        (_ :
          (Quotient.functor (relations W) ⋙ G₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) =
    eqToHom
        (_ :
          (Quotient.functor (relations W) ⋙ G₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })
have hw' := Functor.congr_hom h w
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
hw' :
  G₁.map (wIso w hw✝).hom =
    eqToHom (_ : (MorphismProperty.Q W ⋙ G₁).obj { obj := Y }.obj = (MorphismProperty.Q W ⋙ G₂).obj { obj := Y }.obj) ≫
      G₂.map (wIso w hw✝).hom ≫
        eqToHom
          (_ : (MorphismProperty.Q W ⋙ G₂).obj { obj := X }.obj = (MorphismProperty.Q W ⋙ G₁).obj { obj := X }.obj)
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) =
    eqToHom
        (_ :
          (Quotient.functor (relations W) ⋙ G₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
hw' :
  (MorphismProperty.Q W ⋙ G₁).map w =
    eqToHom (_ : (MorphismProperty.Q W ⋙ G₁).obj { obj := Y }.obj = (MorphismProperty.Q W ⋙ G₂).obj { obj := Y }.obj) ≫
      (MorphismProperty.Q W ⋙ G₂).map w ≫
        eqToHom
          (_ : (MorphismProperty.Q W ⋙ G₂).obj { obj := X }.obj = (MorphismProperty.Q W ⋙ G₁).obj { obj := X }.obj)
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) =
    eqToHom
        (_ :
          (Quotient.functor (relations W) ⋙ G₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })
simp only [Functor.comp_map, hw] at hw'
case h'.refine'_2.mk.mk.inr.mk.refine'_1
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
hw' :
  G₁.map (wIso w hw✝).hom =
    eqToHom (_ : (MorphismProperty.Q W ⋙ G₁).obj { obj := Y }.obj = (MorphismProperty.Q W ⋙ G₂).obj { obj := Y }.obj) ≫
      G₂.map (wIso w hw✝).hom ≫
        eqToHom
          (_ : (MorphismProperty.Q W ⋙ G₂).obj { obj := X }.obj = (MorphismProperty.Q W ⋙ G₁).obj { obj := X }.obj)
⊢ G₁.obj ((MorphismProperty.Q W).obj Y) = G₂.obj ((MorphismProperty.Q W).obj Y)

case h'.refine'_2.mk.mk.inr.mk.refine'_2
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
hw' :
  G₁.map (wIso w hw✝).hom =
    eqToHom (_ : (MorphismProperty.Q W ⋙ G₁).obj { obj := Y }.obj = (MorphismProperty.Q W ⋙ G₂).obj { obj := Y }.obj) ≫
      G₂.map (wIso w hw✝).hom ≫
        eqToHom
          (_ : (MorphismProperty.Q W ⋙ G₂).obj { obj := X }.obj = (MorphismProperty.Q W ⋙ G₁).obj { obj := X }.obj)
⊢ G₁.obj ((MorphismProperty.Q W).obj X) = G₂.obj ((MorphismProperty.Q W).obj X)
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
hw' :
  G₁.map (wIso w hw✝).hom =
    eqToHom (_ : (MorphismProperty.Q W ⋙ G₁).obj { obj := Y }.obj = (MorphismProperty.Q W ⋙ G₂).obj { obj := Y }.obj) ≫
      G₂.map (wIso w hw✝).hom ≫
        eqToHom
          (_ : (MorphismProperty.Q W ⋙ G₂).obj { obj := X }.obj = (MorphismProperty.Q W ⋙ G₁).obj { obj := X }.obj)
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) =
    eqToHom
        (_ :
          (Quotient.functor (relations W) ⋙ G₁).obj { obj := X } =
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := X }) ≫
      (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr { val := w, property := hw✝ })) ≫
        eqToHom
          (_ :
            (Quotient.functor (relations W) ⋙ G₂).obj { obj := Y } =
              (Quotient.functor (relations W) ⋙ G₁).obj { obj := Y })
refine' Functor.congr_inv_of_congr_hom _ _ _ _ _ hw'
no goals
case h'.refine'_2.mk.mk.inr.mk.refine'_1
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
hw' :
  G₁.map (wIso w hw✝).hom =
    eqToHom (_ : (MorphismProperty.Q W ⋙ G₁).obj { obj := Y }.obj = (MorphismProperty.Q W ⋙ G₂).obj { obj := Y }.obj) ≫
      G₂.map (wIso w hw✝).hom ≫
        eqToHom
          (_ : (MorphismProperty.Q W ⋙ G₂).obj { obj := X }.obj = (MorphismProperty.Q W ⋙ G₁).obj { obj := X }.obj)
⊢ G₁.obj ((MorphismProperty.Q W).obj Y) = G₂.obj ((MorphismProperty.Q W).obj Y)

case h'.refine'_2.mk.mk.inr.mk.refine'_2
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
hw' :
  G₁.map (wIso w hw✝).hom =
    eqToHom (_ : (MorphismProperty.Q W ⋙ G₁).obj { obj := Y }.obj = (MorphismProperty.Q W ⋙ G₂).obj { obj := Y }.obj) ≫
      G₂.map (wIso w hw✝).hom ≫
        eqToHom
          (_ : (MorphismProperty.Q W ⋙ G₂).obj { obj := X }.obj = (MorphismProperty.Q W ⋙ G₁).obj { obj := X }.obj)
⊢ G₁.obj ((MorphismProperty.Q W).obj X) = G₂.obj ((MorphismProperty.Q W).obj X)
all_goals apply Functor.congr_obj h
no goals
case h'.refine'_2.mk.mk.inr.mk.refine'_2
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
h : MorphismProperty.Q W ⋙ G₁ = MorphismProperty.Q W ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : (MorphismProperty.Q W).map w = (wIso w hw✝).hom
hw' :
  G₁.map (wIso w hw✝).hom =
    eqToHom (_ : (MorphismProperty.Q W ⋙ G₁).obj { obj := Y }.obj = (MorphismProperty.Q W ⋙ G₂).obj { obj := Y }.obj) ≫
      G₂.map (wIso w hw✝).hom ≫
        eqToHom
          (_ : (MorphismProperty.Q W ⋙ G₂).obj { obj := X }.obj = (MorphismProperty.Q W ⋙ G₁).obj { obj := X }.obj)
⊢ G₁.obj ((MorphismProperty.Q W).obj X) = G₂.obj ((MorphismProperty.Q W).obj X)
apply Functor.congr_obj h