[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.3611, u_2} D
⊢ Category.{?u.3615, u_1} (Localization W)
[PROOFSTEP]
dsimp only [Localization]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.3611, u_2} D
⊢ Category.{?u.3615, u_1} (Quotient (relations W))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.8073, u_2} D
X Y : C
w : X ⟶ Y
hw : W w
⊢ Paths.of.obj { obj := Y } ⟶ Paths.of.obj { obj := X }
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.8073, u_2} D
X Y : C
w : X ⟶ Y
hw : W w
⊢ { obj := Y } ⟶ { obj := X }
[PROOFSTEP]
exact Paths.of.map (Sum.inr ⟨w, hw⟩)
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.11802, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.11824, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ {X Y : LocQuiver W} → (X ⟶ Y) → ((fun X => G.obj X.obj) X ⟶ (fun X => G.obj X.obj) Y)
[PROOFSTEP]
intros X Y
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.11802, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.11824, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : LocQuiver W
⊢ (X ⟶ Y) → ((fun X => G.obj X.obj) X ⟶ (fun X => G.obj X.obj) Y)
[PROOFSTEP]
rintro (f | ⟨g, hg⟩)
[GOAL]
case inl
C : Type u_1
inst✝¹ : Category.{?u.11802, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.11824, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : LocQuiver W
f : X.obj ⟶ Y.obj
⊢ (fun X => G.obj X.obj) X ⟶ (fun X => G.obj X.obj) Y
[PROOFSTEP]
exact G.map f
[GOAL]
case inr.mk
C : Type u_1
inst✝¹ : Category.{?u.11802, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.11824, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : LocQuiver W
g : Y.obj ⟶ X.obj
hg : W g
⊢ (fun X => G.obj X.obj) X ⟶ (fun X => G.obj X.obj) Y
[PROOFSTEP]
haveI := hG g hg
[GOAL]
case inr.mk
C : Type u_1
inst✝¹ : Category.{?u.11802, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.11824, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : LocQuiver W
g : Y.obj ⟶ X.obj
hg : W g
this : IsIso (G.map g)
⊢ (fun X => G.obj X.obj) X ⟶ (fun X => G.obj X.obj) Y
[PROOFSTEP]
exact inv (G.map g)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ ∀ (x y : Paths (LocQuiver W)) (f₁ f₂ : x ⟶ y),
    relations W f₁ f₂ → (liftToPathCategory G hG).map f₁ = (liftToPathCategory G hG).map f₂
[PROOFSTEP]
rintro ⟨X⟩ ⟨Y⟩ f₁ f₂ r
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f₁ f₂ : { obj := X } ⟶ { obj := Y }
r : relations W f₁ f₂
⊢ (liftToPathCategory G hG).map f₁ = (liftToPathCategory G hG).map f₂
[PROOFSTEP]
rcases r with (_ | _ | ⟨f, hf⟩ | ⟨f, hf⟩)
[GOAL]
case mk.mk.id
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ : C
X Y : Paths (LocQuiver W)
⊢ (liftToPathCategory G hG).map (ψ₁ W (𝟙 X✝)) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝))
[PROOFSTEP]
aesop_cat
[GOAL]
case mk.mk.comp
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ Y✝¹ : C
X Y : Paths (LocQuiver W)
Y✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y✝¹
⊢ (liftToPathCategory G hG).map (ψ₁ W (f✝ ≫ g✝)) = (liftToPathCategory G hG).map (ψ₁ W f✝ ≫ ψ₁ W g✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case mk.mk.Winv₁
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ : C
X Y : Paths (LocQuiver W)
Y✝ : C
f : X✝ ⟶ Y✝
hf : W f
⊢ (liftToPathCategory G hG).map (ψ₁ W f ≫ ψ₂ W f hf) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝))
case mk.mk.Winv₂
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝¹ : C
X Y : Paths (LocQuiver W)
X✝ : C
f : X✝ ⟶ X✝¹
hf : W f
⊢ (liftToPathCategory G hG).map (ψ₂ W f hf ≫ ψ₁ W f) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝¹))
[PROOFSTEP]
all_goals
  dsimp
  haveI := hG f hf
  simp
  rfl
[GOAL]
case mk.mk.Winv₁
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ : C
X Y : Paths (LocQuiver W)
Y✝ : C
f : X✝ ⟶ Y✝
hf : W f
⊢ (liftToPathCategory G hG).map (ψ₁ W f ≫ ψ₂ W f hf) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝))
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.Winv₁
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ : C
X Y : Paths (LocQuiver W)
Y✝ : C
f : X✝ ⟶ Y✝
hf : W f
⊢ composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (Quiver.Hom.toPath (Sum.inl f) ≫ Quiver.Hom.toPath (Sum.inr { val := f, property := hf }))) =
    composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (𝟙 (ιPaths W X✝)))
[PROOFSTEP]
haveI := hG f hf
[GOAL]
case mk.mk.Winv₁
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ : C
X Y : Paths (LocQuiver W)
Y✝ : C
f : X✝ ⟶ Y✝
hf : W f
this : IsIso (G.map f)
⊢ composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (Quiver.Hom.toPath (Sum.inl f) ≫ Quiver.Hom.toPath (Sum.inr { val := f, property := hf }))) =
    composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (𝟙 (ιPaths W X✝)))
[PROOFSTEP]
simp
[GOAL]
case mk.mk.Winv₁
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ : C
X Y : Paths (LocQuiver W)
Y✝ : C
f : X✝ ⟶ Y✝
hf : W f
this : IsIso (G.map f)
⊢ 𝟙 (G.obj X✝) =
    composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (𝟙 (ιPaths W X✝)))
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.Winv₂
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝¹ : C
X Y : Paths (LocQuiver W)
X✝ : C
f : X✝ ⟶ X✝¹
hf : W f
⊢ (liftToPathCategory G hG).map (ψ₂ W f hf ≫ ψ₁ W f) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝¹))
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.Winv₂
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝¹ : C
X Y : Paths (LocQuiver W)
X✝ : C
f : X✝ ⟶ X✝¹
hf : W f
⊢ composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (Quiver.Hom.toPath (Sum.inr { val := f, property := hf }) ≫ Quiver.Hom.toPath (Sum.inl f))) =
    composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (𝟙 (ιPaths W X✝¹)))
[PROOFSTEP]
haveI := hG f hf
[GOAL]
case mk.mk.Winv₂
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝¹ : C
X Y : Paths (LocQuiver W)
X✝ : C
f : X✝ ⟶ X✝¹
hf : W f
this : IsIso (G.map f)
⊢ composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (Quiver.Hom.toPath (Sum.inr { val := f, property := hf }) ≫ Quiver.Hom.toPath (Sum.inl f))) =
    composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (𝟙 (ιPaths W X✝¹)))
[PROOFSTEP]
simp
[GOAL]
case mk.mk.Winv₂
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.13221, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝¹ : C
X Y : Paths (LocQuiver W)
X✝ : C
f : X✝ ⟶ X✝¹
hf : W f
this : IsIso (G.map f)
⊢ 𝟙 (G.obj X✝¹) =
    composePath
      (Prefunctor.mapPath
        { obj := fun X => G.obj X.obj,
          map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => inv (G.map ↑val)) a }
        (𝟙 (ιPaths W X✝¹)))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ ∀ (X Y : C) (f : X ⟶ Y),
    (MorphismProperty.Q W ⋙ lift G hG).map f =
      eqToHom (_ : (MorphismProperty.Q W ⋙ lift G hG).obj X = (MorphismProperty.Q W ⋙ lift G hG).obj X) ≫
        G.map f ≫ eqToHom (_ : G.obj Y = (MorphismProperty.Q W ⋙ lift G hG).obj Y)
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f : X ⟶ Y
⊢ (MorphismProperty.Q W ⋙ lift G hG).map f =
    eqToHom (_ : (MorphismProperty.Q W ⋙ lift G hG).obj X = (MorphismProperty.Q W ⋙ lift G hG).obj X) ≫
      G.map f ≫ eqToHom (_ : G.obj Y = (MorphismProperty.Q W ⋙ lift G hG).obj Y)
[PROOFSTEP]
simp only [Functor.comp_map, eqToHom_refl, comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f : X ⟶ Y
⊢ (lift G hG).map ((MorphismProperty.Q W).map f) = G.map f
[PROOFSTEP]
dsimp [MorphismProperty.Q, Quot.liftOn]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X Y : C
f : X ⟶ Y
⊢ composePath (Quiver.Hom.toPath (G.map f)) = G.map f
[PROOFSTEP]
rw [composePath_toPath]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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₂
[PROOFSTEP]
suffices h' : Quotient.functor _ ⋙ G₁ = Quotient.functor _ ⋙ G₂
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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₂
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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
[PROOFSTEP]
rintro ⟨⟨X⟩⟩
[GOAL]
case refine'_1.mk.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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 } }
[PROOFSTEP]
apply Functor.congr_obj h
[GOAL]
case refine'_2
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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)
[PROOFSTEP]
rintro ⟨⟨X⟩⟩ ⟨⟨Y⟩⟩ ⟨f⟩
[GOAL]
case refine'_2.mk.mk.mk.mk.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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 } })
[PROOFSTEP]
apply Functor.congr_hom h'
[GOAL]
case h'
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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₂
[PROOFSTEP]
refine' Paths.ext_functor _ _
[GOAL]
case h'.refine'_1
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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
[PROOFSTEP]
ext X
[GOAL]
case h'.refine'_1.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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
[PROOFSTEP]
cases X
[GOAL]
case h'.refine'_1.h.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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✝ }
[PROOFSTEP]
apply Functor.congr_obj h
[GOAL]
case h'.refine'_2
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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)
[PROOFSTEP]
rintro ⟨X⟩ ⟨Y⟩ (f | ⟨w, hw⟩)
[GOAL]
case h'.refine'_2.mk.mk.inl
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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 })
[PROOFSTEP]
simpa only using Functor.congr_hom h f
[GOAL]
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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 })
[PROOFSTEP]
have hw : W.Q.map w = (wIso w hw).hom := rfl
[GOAL]
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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 })
[PROOFSTEP]
have hw' := Functor.congr_hom h w
[GOAL]
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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 })
[PROOFSTEP]
simp only [Functor.comp_map, hw] at hw'
[GOAL]
case h'.refine'_2.mk.mk.inr.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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 })
[PROOFSTEP]
refine' Functor.congr_inv_of_congr_hom _ _ _ _ _ hw'
[GOAL]
case h'.refine'_2.mk.mk.inr.mk.refine'_1
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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)
[PROOFSTEP]
all_goals apply Functor.congr_obj h
[GOAL]
case h'.refine'_2.mk.mk.inr.mk.refine'_1
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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)
[PROOFSTEP]
apply Functor.congr_obj h
[GOAL]
case h'.refine'_2.mk.mk.inr.mk.refine'_2
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} 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)
[PROOFSTEP]
apply Functor.congr_obj h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.26788, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ Function.RightInverse (fun X => X.as.obj) (MorphismProperty.Q W).toPrefunctor.obj
[PROOFSTEP]
rintro ⟨⟨X⟩⟩
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.26788, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X : C
⊢ (MorphismProperty.Q W).obj ((fun X => X.as.obj) { as := { obj := X } }) = { as := { obj := X } }
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
⊢ P = ⊤
[PROOFSTEP]
funext X Y f
[GOAL]
case h.h.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f = ⊤ f
[PROOFSTEP]
ext
[GOAL]
case h.h.h.a
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f ↔ ⊤ f
[PROOFSTEP]
constructor
[GOAL]
case h.h.h.a.mp
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f → ⊤ f
[PROOFSTEP]
intro
[GOAL]
case h.h.h.a.mp
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : P f
⊢ ⊤ f
[PROOFSTEP]
apply MorphismProperty.top_apply
[GOAL]
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ ⊤ f → P f
[PROOFSTEP]
intro
[GOAL]
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
⊢ P f
[PROOFSTEP]
let G : _ ⥤ W.Localization := Quotient.functor _
[GOAL]
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
⊢ P f
[PROOFSTEP]
haveI : Full G := Quotient.fullFunctor _
[GOAL]
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
⊢ P f
[PROOFSTEP]
suffices ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
  by
  rcases X with ⟨⟨X⟩⟩
  rcases Y with ⟨⟨Y⟩⟩
  simpa only [Functor.image_preimage] using this _ _ (G.preimage f)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this✝ : Full G
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
⊢ P f
[PROOFSTEP]
rcases X with ⟨⟨X⟩⟩
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
Y : MorphismProperty.Localization W
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this✝ : Full G
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
X : C
f : { as := { obj := X } } ⟶ Y
a✝ : ⊤ f
⊢ P f
[PROOFSTEP]
rcases Y with ⟨⟨Y⟩⟩
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this✝ : Full G
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
X Y : C
f : { as := { obj := X } } ⟶ { as := { obj := Y } }
a✝ : ⊤ f
⊢ P f
[PROOFSTEP]
simpa only [Functor.image_preimage] using this _ _ (G.preimage f)
[GOAL]
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
⊢ ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
[PROOFSTEP]
intros X₁ X₂ p
[GOAL]
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂ : Paths (LocQuiver W)
p : X₁ ⟶ X₂
⊢ P (G.map p)
[PROOFSTEP]
induction' p with X₂ X₃ p g hp
[GOAL]
case h.h.h.a.mpr.nil
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂ : Paths (LocQuiver W)
⊢ P (G.map Quiver.Path.nil)
[PROOFSTEP]
simpa only [Functor.map_id] using hP₁ (𝟙 X₁.obj)
[GOAL]
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
⊢ P (G.map (Quiver.Path.cons p g))
[PROOFSTEP]
let p' : X₁ ⟶ X₂ := p
[GOAL]
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (Quiver.Path.cons p g))
[PROOFSTEP]
rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ Quiver.Path.cons p' g = p' ≫ Quiver.Hom.toPath g
[PROOFSTEP]
rfl
[GOAL]
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map p' ≫ G.map (Quiver.Hom.toPath g))
[PROOFSTEP]
refine' hP₃ _ _ hp _
[GOAL]
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (Quiver.Hom.toPath g))
[PROOFSTEP]
rcases g with (g | ⟨g, hg⟩)
[GOAL]
case h.h.h.a.mpr.cons.inl
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₂.obj ⟶ X₃.obj
⊢ P (G.map (Quiver.Hom.toPath (Sum.inl g)))
[PROOFSTEP]
apply hP₁
[GOAL]
case h.h.h.a.mpr.cons.inr.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.27652, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj ⟶ X₂.obj
hg : W g
⊢ P (G.map (Quiver.Hom.toPath (Sum.inr { val := g, property := hg })))
[PROOFSTEP]
apply hP₂
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F₁ F₂ : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F₁ ⟶ MorphismProperty.Q W ⋙ F₂
X : C
⊢ app τ ((MorphismProperty.Q W).obj X) = NatTrans.app τ X
[PROOFSTEP]
simp only [app, eqToHom_refl, comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F₁ F₂ : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F₁ ⟶ MorphismProperty.Q W ⋙ F₂
X : C
⊢ NatTrans.app τ (Equiv.invFun (objEquiv W) ((MorphismProperty.Q W).obj X)) = NatTrans.app τ X
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.36397, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F₁ F₂ : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F₁ ⟶ MorphismProperty.Q W ⋙ F₂
⊢ ∀ ⦃X Y : MorphismProperty.Localization W⦄ (f : X ⟶ Y),
    F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f
[PROOFSTEP]
suffices MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
  by
  intro X Y f
  simpa only [← this] using MorphismProperty.top_apply f
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.36397, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F₁ F₂ : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F₁ ⟶ MorphismProperty.Q W ⋙ F₂
this : MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
⊢ ∀ ⦃X Y : MorphismProperty.Localization W⦄ (f : X ⟶ Y),
    F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.36397, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F₁ F₂ : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F₁ ⟶ MorphismProperty.Q W ⋙ F₂
this : MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f
[PROOFSTEP]
simpa only [← this] using MorphismProperty.top_apply f
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.36397, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F₁ F₂ : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F₁ ⟶ MorphismProperty.Q W ⋙ F₂
⊢ MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
[PROOFSTEP]
refine'
  morphismProperty_is_top' (MorphismProperty.naturalityProperty (NatTransExtension.app τ)) _
    (MorphismProperty.naturalityProperty.stableUnderInverse _)
    (MorphismProperty.naturalityProperty.stableUnderComposition _)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.36397, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F₁ F₂ : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F₁ ⟶ MorphismProperty.Q W ⋙ F₂
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.naturalityProperty (NatTransExtension.app τ) ((MorphismProperty.Q W).map f)
[PROOFSTEP]
intros X Y f
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.36397, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F₁ F₂ : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F₁ ⟶ MorphismProperty.Q W ⋙ F₂
X Y : C
f : X ⟶ Y
⊢ MorphismProperty.naturalityProperty (NatTransExtension.app τ) ((MorphismProperty.Q W).map f)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.36397, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F₁ F₂ : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F₁ ⟶ MorphismProperty.Q W ⋙ F₂
X Y : C
f : X ⟶ Y
⊢ F₁.map ((MorphismProperty.Q W).map f) ≫ NatTransExtension.app τ ((MorphismProperty.Q W).obj Y) =
    NatTransExtension.app τ ((MorphismProperty.Q W).obj X) ≫ F₂.map ((MorphismProperty.Q W).map f)
[PROOFSTEP]
simpa only [NatTransExtension.app_eq] using τ.naturality f
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
F G : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F ⟶ MorphismProperty.Q W ⋙ G
⊢ 𝟙 (MorphismProperty.Q W) ◫ natTransExtension τ = τ
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
F G : MorphismProperty.Localization W ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
⊢ τ₁ = τ₂
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
F G : MorphismProperty.Localization W ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
X : MorphismProperty.Localization W
⊢ NatTrans.app τ₁ X = NatTrans.app τ₂ X
[PROOFSTEP]
have eq := (objEquiv W).right_inv X
[GOAL]
case w.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
F G : MorphismProperty.Localization W ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
X : MorphismProperty.Localization W
eq : Equiv.toFun (objEquiv W) (Equiv.invFun (objEquiv W) X) = X
⊢ NatTrans.app τ₁ X = NatTrans.app τ₂ X
[PROOFSTEP]
simp only [objEquiv] at eq
[GOAL]
case w.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
F G : MorphismProperty.Localization W ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
X : MorphismProperty.Localization W
eq : (MorphismProperty.Q W).obj X.as.obj = X
⊢ NatTrans.app τ₁ X = NatTrans.app τ₂ X
[PROOFSTEP]
rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.49983, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ Y✝ : MorphismProperty.FunctorsInverting W D
τ : X✝ ⟶ Y✝
⊢ MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X✝ = X✝.obj
[PROOFSTEP]
rw [fac]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.49983, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ Y✝ : MorphismProperty.FunctorsInverting W D
τ : X✝ ⟶ Y✝
⊢ Y✝.obj = MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y✝
[PROOFSTEP]
rw [fac]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.49983, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
G : MorphismProperty.FunctorsInverting W D
⊢ 𝟙 (MorphismProperty.Q W) ◫
      { obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
            map := fun {X Y} τ =>
              natTransExtension
                (eqToHom
                    (_ :
                      MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                        X.obj) ≫
                  τ ≫
                    eqToHom
                      (_ :
                        Y.obj =
                          MorphismProperty.Q W ⋙
                            (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.map
        (𝟙 G) =
    𝟙 (MorphismProperty.Q W) ◫
      𝟙
        ({ obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
              map := fun {X Y} τ =>
                natTransExtension
                  (eqToHom
                      (_ :
                        MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                          X.obj) ≫
                    τ ≫
                      eqToHom
                        (_ :
                          Y.obj =
                            MorphismProperty.Q W ⋙
                              (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.obj
          G)
[PROOFSTEP]
rw [natTransExtension_hcomp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.49983, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
G : MorphismProperty.FunctorsInverting W D
⊢ eqToHom (_ : MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) G = G.obj) ≫
      𝟙 G ≫
        eqToHom
          (_ : G.obj = MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) G) =
    𝟙 (MorphismProperty.Q W) ◫
      𝟙
        ({ obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
              map := fun {X Y} τ =>
                natTransExtension
                  (eqToHom
                      (_ :
                        MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                          X.obj) ≫
                    τ ≫
                      eqToHom
                        (_ :
                          Y.obj =
                            MorphismProperty.Q W ⋙
                              (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.obj
          G)
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.49983, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
G : MorphismProperty.FunctorsInverting W D
X : C
⊢ NatTrans.app
      (eqToHom
          (_ : MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) G = G.obj) ≫
        𝟙 G ≫
          eqToHom
            (_ : G.obj = MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) G))
      X =
    NatTrans.app
      (𝟙 (MorphismProperty.Q W) ◫
        𝟙
          ({ obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
                map := fun {X Y} τ =>
                  natTransExtension
                    (eqToHom
                        (_ :
                          MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                            X.obj) ≫
                      τ ≫
                        eqToHom
                          (_ :
                            Y.obj =
                              MorphismProperty.Q W ⋙
                                (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.obj
            G))
      X
[PROOFSTEP]
simp only [NatTrans.comp_app, eqToHom_app, eqToHom_refl, comp_id, id_comp, NatTrans.hcomp_id_app, NatTrans.id_app,
  Functor.map_id]
[GOAL]
case w.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.49983, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
G : MorphismProperty.FunctorsInverting W D
X : C
⊢ NatTrans.app (𝟙 G) X = 𝟙 ((lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)).obj ((MorphismProperty.Q W).obj X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.49983, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ Y✝ Z✝ : MorphismProperty.FunctorsInverting W D
τ₁ : X✝ ⟶ Y✝
τ₂ : Y✝ ⟶ Z✝
⊢ 𝟙 (MorphismProperty.Q W) ◫
      { obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
            map := fun {X Y} τ =>
              natTransExtension
                (eqToHom
                    (_ :
                      MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                        X.obj) ≫
                  τ ≫
                    eqToHom
                      (_ :
                        Y.obj =
                          MorphismProperty.Q W ⋙
                            (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.map
        (τ₁ ≫ τ₂) =
    𝟙 (MorphismProperty.Q W) ◫
      ({ obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
              map := fun {X Y} τ =>
                natTransExtension
                  (eqToHom
                      (_ :
                        MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                          X.obj) ≫
                    τ ≫
                      eqToHom
                        (_ :
                          Y.obj =
                            MorphismProperty.Q W ⋙
                              (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.map
          τ₁ ≫
        { obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
              map := fun {X Y} τ =>
                natTransExtension
                  (eqToHom
                      (_ :
                        MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                          X.obj) ≫
                    τ ≫
                      eqToHom
                        (_ :
                          Y.obj =
                            MorphismProperty.Q W ⋙
                              (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.map
          τ₂)
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.49983, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ Y✝ Z✝ : MorphismProperty.FunctorsInverting W D
τ₁ : X✝ ⟶ Y✝
τ₂ : Y✝ ⟶ Z✝
X : C
⊢ NatTrans.app
      (𝟙 (MorphismProperty.Q W) ◫
        { obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
              map := fun {X Y} τ =>
                natTransExtension
                  (eqToHom
                      (_ :
                        MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                          X.obj) ≫
                    τ ≫
                      eqToHom
                        (_ :
                          Y.obj =
                            MorphismProperty.Q W ⋙
                              (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.map
          (τ₁ ≫ τ₂))
      X =
    NatTrans.app
      (𝟙 (MorphismProperty.Q W) ◫
        ({ obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
                map := fun {X Y} τ =>
                  natTransExtension
                    (eqToHom
                        (_ :
                          MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                            X.obj) ≫
                      τ ≫
                        eqToHom
                          (_ :
                            Y.obj =
                              MorphismProperty.Q W ⋙
                                (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.map
            τ₁ ≫
          { obj := fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj),
                map := fun {X Y} τ =>
                  natTransExtension
                    (eqToHom
                        (_ :
                          MorphismProperty.Q W ⋙ (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) X =
                            X.obj) ≫
                      τ ≫
                        eqToHom
                          (_ :
                            Y.obj =
                              MorphismProperty.Q W ⋙
                                (fun G => lift G.obj (_ : MorphismProperty.IsInvertedBy W G.obj)) Y)) }.map
            τ₂))
      X
[PROOFSTEP]
simp only [natTransExtension_hcomp, NatTrans.comp_app, eqToHom_app, eqToHom_refl, id_comp, comp_id, NatTrans.hcomp_app,
  NatTrans.id_app, Functor.map_id, natTransExtension_app, NatTransExtension.app_eq]
[GOAL]
case w.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.49983, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
X✝ Y✝ Z✝ : MorphismProperty.FunctorsInverting W D
τ₁ : X✝ ⟶ Y✝
τ₂ : Y✝ ⟶ Z✝
X : C
⊢ NatTrans.app (τ₁ ≫ τ₂) X = NatTrans.app τ₁ X ≫ NatTrans.app τ₂ X
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.63998, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ 𝟭 (MorphismProperty.Localization W ⥤ D) = functor W D ⋙ inverse W D
[PROOFSTEP]
refine' Functor.ext (fun G => _) fun G₁ G₂ τ => _
[GOAL]
case refine'_1
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.63998, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
G : MorphismProperty.Localization W ⥤ D
⊢ (𝟭 (MorphismProperty.Localization W ⥤ D)).obj G = (functor W D ⋙ inverse W D).obj G
[PROOFSTEP]
apply uniq
[GOAL]
case refine'_1.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.63998, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
G : MorphismProperty.Localization W ⥤ D
⊢ MorphismProperty.Q W ⋙ (𝟭 (MorphismProperty.Localization W ⥤ D)).obj G =
    MorphismProperty.Q W ⋙ (functor W D ⋙ inverse W D).obj G
[PROOFSTEP]
dsimp [Functor]
[GOAL]
case refine'_1.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.63998, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
G : MorphismProperty.Localization W ⥤ D
⊢ MorphismProperty.Q W ⋙ G = MorphismProperty.Q W ⋙ (inverse W D).obj ((functor W D).obj G)
[PROOFSTEP]
erw [fac]
[GOAL]
case refine'_1.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.63998, u_2} D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
G : MorphismProperty.Localization W ⥤ D
⊢ MorphismProperty.Q W ⋙ G = ((functor W D).obj G).obj
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.63998, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
τ : G₁ ⟶ G₂
⊢ (𝟭 (MorphismProperty.Localization W ⥤ D)).map τ =
    eqToHom (_ : (𝟭 (MorphismProperty.Localization W ⥤ D)).obj G₁ = (functor W D ⋙ inverse W D).obj G₁) ≫
      (functor W D ⋙ inverse W D).map τ ≫
        eqToHom (_ : (functor W D ⋙ inverse W D).obj G₂ = (𝟭 (MorphismProperty.Localization W ⥤ D)).obj G₂)
[PROOFSTEP]
apply natTrans_hcomp_injective
[GOAL]
case refine'_2.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.63998, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
τ : G₁ ⟶ G₂
⊢ 𝟙 (MorphismProperty.Q W) ◫ (𝟭 (MorphismProperty.Localization W ⥤ D)).map τ =
    𝟙 (MorphismProperty.Q W) ◫
      (eqToHom (_ : (𝟭 (MorphismProperty.Localization W ⥤ D)).obj G₁ = (functor W D ⋙ inverse W D).obj G₁) ≫
        (functor W D ⋙ inverse W D).map τ ≫
          eqToHom (_ : (functor W D ⋙ inverse W D).obj G₂ = (𝟭 (MorphismProperty.Localization W ⥤ D)).obj G₂))
[PROOFSTEP]
ext X
[GOAL]
case refine'_2.h.w.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.63998, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ G₂ : MorphismProperty.Localization W ⥤ D
τ : G₁ ⟶ G₂
X : C
⊢ NatTrans.app (𝟙 (MorphismProperty.Q W) ◫ (𝟭 (MorphismProperty.Localization W ⥤ D)).map τ) X =
    NatTrans.app
      (𝟙 (MorphismProperty.Q W) ◫
        (eqToHom (_ : (𝟭 (MorphismProperty.Localization W ⥤ D)).obj G₁ = (functor W D ⋙ inverse W D).obj G₁) ≫
          (functor W D ⋙ inverse W D).map τ ≫
            eqToHom (_ : (functor W D ⋙ inverse W D).obj G₂ = (𝟭 (MorphismProperty.Localization W ⥤ D)).obj G₂)))
      X
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.72185, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ inverse W D ⋙ functor W D = 𝟭 (MorphismProperty.FunctorsInverting W D)
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.72185, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ ∀ (X : MorphismProperty.FunctorsInverting W D),
    (inverse W D ⋙ functor W D).obj X = (𝟭 (MorphismProperty.FunctorsInverting W D)).obj X
[PROOFSTEP]
rintro ⟨G, hG⟩
[GOAL]
case refine'_1.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.72185, u_2} D
G✝ : C ⥤ D
hG✝ : MorphismProperty.IsInvertedBy W G✝
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ (inverse W D ⋙ functor W D).obj { obj := G, property := hG } =
    (𝟭 (MorphismProperty.FunctorsInverting W D)).obj { obj := G, property := hG }
[PROOFSTEP]
ext
[GOAL]
case refine'_1.mk.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.72185, u_2} D
G✝ : C ⥤ D
hG✝ : MorphismProperty.IsInvertedBy W G✝
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ ((inverse W D ⋙ functor W D).obj { obj := G, property := hG }).obj =
    ((𝟭 (MorphismProperty.FunctorsInverting W D)).obj { obj := G, property := hG }).obj
[PROOFSTEP]
exact fac G hG
[GOAL]
case refine'_2
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.72185, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
⊢ ∀ (X Y : MorphismProperty.FunctorsInverting W D) (f : X ⟶ Y),
    (inverse W D ⋙ functor W D).map f =
      eqToHom (_ : (inverse W D ⋙ functor W D).obj X = (𝟭 (MorphismProperty.FunctorsInverting W D)).obj X) ≫
        (𝟭 (MorphismProperty.FunctorsInverting W D)).map f ≫
          eqToHom (_ : (𝟭 (MorphismProperty.FunctorsInverting W D)).obj Y = (inverse W D ⋙ functor W D).obj Y)
[PROOFSTEP]
rintro ⟨G₁, hG₁⟩ ⟨G₂, hG₂⟩ f
[GOAL]
case refine'_2.mk.mk
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.72185, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ : C ⥤ D
hG₁ : MorphismProperty.IsInvertedBy W G₁
G₂ : C ⥤ D
hG₂ : MorphismProperty.IsInvertedBy W G₂
f : { obj := G₁, property := hG₁ } ⟶ { obj := G₂, property := hG₂ }
⊢ (inverse W D ⋙ functor W D).map f =
    eqToHom
        (_ :
          (inverse W D ⋙ functor W D).obj { obj := G₁, property := hG₁ } =
            (𝟭 (MorphismProperty.FunctorsInverting W D)).obj { obj := G₁, property := hG₁ }) ≫
      (𝟭 (MorphismProperty.FunctorsInverting W D)).map f ≫
        eqToHom
          (_ :
            (𝟭 (MorphismProperty.FunctorsInverting W D)).obj { obj := G₂, property := hG₂ } =
              (inverse W D ⋙ functor W D).obj { obj := G₂, property := hG₂ })
[PROOFSTEP]
ext
[GOAL]
case refine'_2.mk.mk.h.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.72185, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
G₁ : C ⥤ D
hG₁ : MorphismProperty.IsInvertedBy W G₁
G₂ : C ⥤ D
hG₂ : MorphismProperty.IsInvertedBy W G₂
f : { obj := G₁, property := hG₁ } ⟶ { obj := G₂, property := hG₂ }
x✝ : C
⊢ NatTrans.app ((inverse W D ⋙ functor W D).map f) x✝ =
    NatTrans.app
      (eqToHom
          (_ :
            (inverse W D ⋙ functor W D).obj { obj := G₁, property := hG₁ } =
              (𝟭 (MorphismProperty.FunctorsInverting W D)).obj { obj := G₁, property := hG₁ }) ≫
        (𝟭 (MorphismProperty.FunctorsInverting W D)).map f ≫
          eqToHom
            (_ :
              (𝟭 (MorphismProperty.FunctorsInverting W D)).obj { obj := G₂, property := hG₂ } =
                (inverse W D ⋙ functor W D).obj { obj := G₂, property := hG₂ }))
      x✝
[PROOFSTEP]
apply NatTransExtension.app_eq
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.75061, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F : MorphismProperty.Localization W ⥤ D
⊢ (WhiskeringLeftEquivalence.functor W D).map (NatTrans.app (WhiskeringLeftEquivalence.unitIso W D).hom F) ≫
      NatTrans.app (WhiskeringLeftEquivalence.counitIso W D).hom ((WhiskeringLeftEquivalence.functor W D).obj F) =
    𝟙 ((WhiskeringLeftEquivalence.functor W D).obj F)
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.75061, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F : MorphismProperty.Localization W ⥤ D
x✝ : C
⊢ NatTrans.app
      ((WhiskeringLeftEquivalence.functor W D).map (NatTrans.app (WhiskeringLeftEquivalence.unitIso W D).hom F) ≫
        NatTrans.app (WhiskeringLeftEquivalence.counitIso W D).hom ((WhiskeringLeftEquivalence.functor W D).obj F))
      x✝ =
    NatTrans.app (𝟙 ((WhiskeringLeftEquivalence.functor W D).obj F)) x✝
[PROOFSTEP]
simp only [WhiskeringLeftEquivalence.unitIso_hom, eqToHom_app, eqToHom_refl, WhiskeringLeftEquivalence.counitIso_hom,
  eqToHom_map, eqToHom_trans]
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{u_1, u_1} C
W : MorphismProperty C
D : Type u_2
inst✝ : Category.{?u.75061, u_2} D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
F : MorphismProperty.Localization W ⥤ D
x✝ : C
⊢ NatTrans.app (𝟙 ((WhiskeringLeftEquivalence.functor W D).obj ((𝟭 (MorphismProperty.Localization W ⥤ D)).obj F))) x✝ =
    NatTrans.app (𝟙 ((WhiskeringLeftEquivalence.functor W D).obj F)) x✝
[PROOFSTEP]
rfl


[GOAL]
V : QuivCat
⊢ { obj := fun V => of (Paths ↑V),
          map := fun {X Y} F =>
            Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
      (𝟙 V) =
    𝟙
      ({ obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
        V)
[PROOFSTEP]
change (show Paths V ⥤ _ from _) = _
[GOAL]
V : QuivCat
⊢ (let_fun this :=
      { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        (𝟙 V);
    this) =
    𝟙
      ({ obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
        V)
[PROOFSTEP]
ext
[GOAL]
case h_obj.h
V : QuivCat
x✝ : Paths ↑V
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).obj
      x✝ =
    (𝟙
          ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
            V)).obj
      x✝
case h
V : QuivCat
a✝ b✝ : ↑V
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    (𝟙 V);
                this).obj
              a✝ =
            (𝟙
                  ({ obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                    V)).obj
              a✝) ≫
      (𝟙
              ({ obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                V)).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            (𝟙
                    ({ obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                      V)).obj
                b✝ =
              (let_fun this :=
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      (𝟙 V);
                  this).obj
                b✝)
[PROOFSTEP]
swap
[GOAL]
case h
V : QuivCat
a✝ b✝ : ↑V
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    (𝟙 V);
                this).obj
              a✝ =
            (𝟙
                  ({ obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                    V)).obj
              a✝) ≫
      (𝟙
              ({ obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                V)).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            (𝟙
                    ({ obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                      V)).obj
                b✝ =
              (let_fun this :=
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      (𝟙 V);
                  this).obj
                b✝)
case h_obj.h
V : QuivCat
x✝ : Paths ↑V
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).obj
      x✝ =
    (𝟙
          ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
            V)).obj
      x✝
[PROOFSTEP]
apply eq_conj_eqToHom
[GOAL]
case h_obj.h
V : QuivCat
x✝ : Paths ↑V
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).obj
      x✝ =
    (𝟙
          ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
            V)).obj
      x✝
[PROOFSTEP]
rfl
[GOAL]
U x✝¹ x✝ : QuivCat
F : U ⟶ x✝¹
G : x✝¹ ⟶ x✝
⊢ { obj := fun V => of (Paths ↑V),
          map := fun {X Y} F =>
            Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
      (F ≫ G) =
    { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        F ≫
      { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        G
[PROOFSTEP]
change (show Paths U ⥤ _ from _) = _
[GOAL]
U x✝¹ x✝ : QuivCat
F : U ⟶ x✝¹
G : x✝¹ ⟶ x✝
⊢ (let_fun this :=
      { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        (F ≫ G);
    this) =
    { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        F ≫
      { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        G
[PROOFSTEP]
ext
[GOAL]
case h_obj.h
U x✝² x✝¹ : QuivCat
F : U ⟶ x✝²
G : x✝² ⟶ x✝¹
x✝ : Paths ↑U
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).obj
      x✝ =
    ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            F ≫
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            G).obj
      x✝
case h
U x✝¹ x✝ : QuivCat
F : U ⟶ x✝¹
G : x✝¹ ⟶ x✝
a✝ b✝ : ↑U
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    (F ≫ G);
                this).obj
              a✝ =
            ({ obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    F ≫
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    G).obj
              a✝) ≫
      ({ obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                F ≫
              { obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                G).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            ({ obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      F ≫
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      G).obj
                b✝ =
              (let_fun this :=
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      (F ≫ G);
                  this).obj
                b✝)
[PROOFSTEP]
swap
[GOAL]
case h
U x✝¹ x✝ : QuivCat
F : U ⟶ x✝¹
G : x✝¹ ⟶ x✝
a✝ b✝ : ↑U
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    (F ≫ G);
                this).obj
              a✝ =
            ({ obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    F ≫
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    G).obj
              a✝) ≫
      ({ obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                F ≫
              { obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                G).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            ({ obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      F ≫
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      G).obj
                b✝ =
              (let_fun this :=
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      (F ≫ G);
                  this).obj
                b✝)
case h_obj.h
U x✝² x✝¹ : QuivCat
F : U ⟶ x✝²
G : x✝² ⟶ x✝¹
x✝ : Paths ↑U
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).obj
      x✝ =
    ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            F ≫
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            G).obj
      x✝
[PROOFSTEP]
apply eq_conj_eqToHom
[GOAL]
case h_obj.h
U x✝² x✝¹ : QuivCat
F : U ⟶ x✝²
G : x✝² ⟶ x✝¹
x✝ : Paths ↑U
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).obj
      x✝ =
    ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            F ≫
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            G).obj
      x✝
[PROOFSTEP]
rfl
[GOAL]
V : QuivCat
C : Cat
F : Cat.free.obj V ⟶ C
⊢ ∀ (a b : ↑V) (e : a ⟶ b),
    ((fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F)).map (Quiver.Hom.toPath e) =
      eqToHom (_ : ((fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F)).obj a = F.obj a) ≫
        F.map (Quiver.Hom.toPath e) ≫
          eqToHom (_ : F.obj b = ((fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F)).obj b)
[PROOFSTEP]
simp
[GOAL]
V : QuivCat
C : Cat
⊢ Function.RightInverse (fun F => lift F) fun F => Paths.of ⋙q F.toPrefunctor
[PROOFSTEP]
rintro ⟨obj, map⟩
[GOAL]
case mk
V : QuivCat
C : Cat
obj : ↑V → ↑(forget.obj C)
map : {X Y : ↑V} → (X ⟶ Y) → (obj X ⟶ obj Y)
⊢ (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) { obj := obj, map := map }) = { obj := obj, map := map }
[PROOFSTEP]
dsimp only [Prefunctor.comp]
[GOAL]
case mk
V : QuivCat
C : Cat
obj : ↑V → ↑(forget.obj C)
map : {X Y : ↑V} → (X ⟶ Y) → (obj X ⟶ obj Y)
⊢ { obj := fun X => (lift { obj := obj, map := map }).obj (Paths.of.obj X),
      map := fun {X Y} f => (lift { obj := obj, map := map }).map (Paths.of.map f) } =
    { obj := obj, map := map }
[PROOFSTEP]
congr
[GOAL]
case mk.e_map
V : QuivCat
C : Cat
obj : ↑V → ↑(forget.obj C)
map : {X Y : ↑V} → (X ⟶ Y) → (obj X ⟶ obj Y)
⊢ (fun {X Y} f => (lift { obj := obj, map := map }).map (Paths.of.map f)) = map
[PROOFSTEP]
funext X Y f
[GOAL]
case mk.e_map.h.h.h
V : QuivCat
C : Cat
obj : ↑V → ↑(forget.obj C)
map : {X Y : ↑V} → (X ⟶ Y) → (obj X ⟶ obj Y)
X Y : ↑V
f : X ⟶ Y
⊢ (lift { obj := obj, map := map }).map (Paths.of.map f) = map f
[PROOFSTEP]
exact Category.id_comp _
[GOAL]
V x✝¹ : QuivCat
x✝ : Cat
f : V ⟶ x✝¹
g : x✝¹ ⟶ forget.obj x✝
⊢ ↑((fun V C =>
              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                left_inv :=
                  (_ : ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                right_inv :=
                  (_ : ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
            V x✝).symm
      (f ≫ g) =
    Cat.free.map f ≫
      ↑((fun V C =>
                { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                  left_inv :=
                    (_ : ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                  right_inv :=
                    (_ : ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
              x✝¹ x✝).symm
        g
[PROOFSTEP]
change (show Paths V ⥤ _ from _) = _
[GOAL]
V x✝¹ : QuivCat
x✝ : Cat
f : V ⟶ x✝¹
g : x✝¹ ⟶ forget.obj x✝
⊢ (let_fun this :=
      ↑((fun V C =>
                { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                  left_inv :=
                    (_ : ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                  right_inv :=
                    (_ : ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
              V x✝).symm
        (f ≫ g);
    this) =
    Cat.free.map f ≫
      ↑((fun V C =>
                { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                  left_inv :=
                    (_ : ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                  right_inv :=
                    (_ : ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
              x✝¹ x✝).symm
        g
[PROOFSTEP]
ext
[GOAL]
case h_obj.h
V x✝² : QuivCat
x✝¹ : Cat
f : V ⟶ x✝²
g : x✝² ⟶ forget.obj x✝¹
x✝ : Paths ↑V
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝¹).symm
            (f ≫ g);
        this).obj
      x✝ =
    (Cat.free.map f ≫
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  x✝² x✝¹).symm
            g).obj
      x✝
case h
V x✝¹ : QuivCat
x✝ : Cat
f : V ⟶ x✝¹
g : x✝¹ ⟶ forget.obj x✝
a✝ b✝ : ↑V
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝).symm
            (f ≫ g);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  ↑((fun V C =>
                            { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                              left_inv :=
                                (_ :
                                  ∀ (F : Cat.free.obj V ⟶ C),
                                    (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                              right_inv :=
                                (_ :
                                  ∀ (x : V ⟶ forget.obj C),
                                    (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                          V x✝).symm
                    (f ≫ g);
                this).obj
              a✝ =
            (Cat.free.map f ≫
                  ↑((fun V C =>
                            { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                              left_inv :=
                                (_ :
                                  ∀ (F : Cat.free.obj V ⟶ C),
                                    (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                              right_inv :=
                                (_ :
                                  ∀ (x : V ⟶ forget.obj C),
                                    (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                          x✝¹ x✝).symm
                    g).obj
              a✝) ≫
      (Cat.free.map f ≫
              ↑((fun V C =>
                        { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                          left_inv :=
                            (_ :
                              ∀ (F : Cat.free.obj V ⟶ C),
                                (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                          right_inv :=
                            (_ :
                              ∀ (x : V ⟶ forget.obj C),
                                (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                      x✝¹ x✝).symm
                g).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            (Cat.free.map f ≫
                    ↑((fun V C =>
                              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                                left_inv :=
                                  (_ :
                                    ∀ (F : Cat.free.obj V ⟶ C),
                                      (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                                right_inv :=
                                  (_ :
                                    ∀ (x : V ⟶ forget.obj C),
                                      (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                            x✝¹ x✝).symm
                      g).obj
                b✝ =
              (let_fun this :=
                    ↑((fun V C =>
                              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                                left_inv :=
                                  (_ :
                                    ∀ (F : Cat.free.obj V ⟶ C),
                                      (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                                right_inv :=
                                  (_ :
                                    ∀ (x : V ⟶ forget.obj C),
                                      (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                            V x✝).symm
                      (f ≫ g);
                  this).obj
                b✝)
[PROOFSTEP]
swap
[GOAL]
case h
V x✝¹ : QuivCat
x✝ : Cat
f : V ⟶ x✝¹
g : x✝¹ ⟶ forget.obj x✝
a✝ b✝ : ↑V
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝).symm
            (f ≫ g);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  ↑((fun V C =>
                            { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                              left_inv :=
                                (_ :
                                  ∀ (F : Cat.free.obj V ⟶ C),
                                    (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                              right_inv :=
                                (_ :
                                  ∀ (x : V ⟶ forget.obj C),
                                    (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                          V x✝).symm
                    (f ≫ g);
                this).obj
              a✝ =
            (Cat.free.map f ≫
                  ↑((fun V C =>
                            { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                              left_inv :=
                                (_ :
                                  ∀ (F : Cat.free.obj V ⟶ C),
                                    (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                              right_inv :=
                                (_ :
                                  ∀ (x : V ⟶ forget.obj C),
                                    (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                          x✝¹ x✝).symm
                    g).obj
              a✝) ≫
      (Cat.free.map f ≫
              ↑((fun V C =>
                        { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                          left_inv :=
                            (_ :
                              ∀ (F : Cat.free.obj V ⟶ C),
                                (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                          right_inv :=
                            (_ :
                              ∀ (x : V ⟶ forget.obj C),
                                (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                      x✝¹ x✝).symm
                g).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            (Cat.free.map f ≫
                    ↑((fun V C =>
                              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                                left_inv :=
                                  (_ :
                                    ∀ (F : Cat.free.obj V ⟶ C),
                                      (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                                right_inv :=
                                  (_ :
                                    ∀ (x : V ⟶ forget.obj C),
                                      (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                            x✝¹ x✝).symm
                      g).obj
                b✝ =
              (let_fun this :=
                    ↑((fun V C =>
                              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                                left_inv :=
                                  (_ :
                                    ∀ (F : Cat.free.obj V ⟶ C),
                                      (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                                right_inv :=
                                  (_ :
                                    ∀ (x : V ⟶ forget.obj C),
                                      (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                            V x✝).symm
                      (f ≫ g);
                  this).obj
                b✝)
case h_obj.h
V x✝² : QuivCat
x✝¹ : Cat
f : V ⟶ x✝²
g : x✝² ⟶ forget.obj x✝¹
x✝ : Paths ↑V
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝¹).symm
            (f ≫ g);
        this).obj
      x✝ =
    (Cat.free.map f ≫
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  x✝² x✝¹).symm
            g).obj
      x✝
[PROOFSTEP]
apply eq_conj_eqToHom
[GOAL]
case h_obj.h
V x✝² : QuivCat
x✝¹ : Cat
f : V ⟶ x✝²
g : x✝² ⟶ forget.obj x✝¹
x✝ : Paths ↑V
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝¹).symm
            (f ≫ g);
        this).obj
      x✝ =
    (Cat.free.map f ≫
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  x✝² x✝¹).symm
            g).obj
      x✝
[PROOFSTEP]
rfl