[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X : Paths V
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (𝟙 X) =
    𝟙
      ({ obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.obj
        X)
[PROOFSTEP]
rfl
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map g
[PROOFSTEP]
induction' g with _ _ g' p ih _ _ _
[GOAL]
case nil
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ Quiver.Path.nil) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        Quiver.Path.nil
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
case nil
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ Quiver.Path.nil) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f
[PROOFSTEP]
rfl
[GOAL]
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g') =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        g'
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ Quiver.Path.cons g' p) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        (Quiver.Path.cons g' p)
[PROOFSTEP]
have : f ≫ Quiver.Path.cons g' p = (f ≫ g').cons p := by apply Quiver.Path.comp_cons
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g') =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        g'
⊢ f ≫ Quiver.Path.cons g' p = Quiver.Path.cons (f ≫ g') p
[PROOFSTEP]
apply Quiver.Path.comp_cons
[GOAL]
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g') =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        g'
this : f ≫ Quiver.Path.cons g' p = Quiver.Path.cons (f ≫ g') p
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ Quiver.Path.cons g' p) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        (Quiver.Path.cons g' p)
[PROOFSTEP]
rw [this]
[GOAL]
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g') =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        g'
this : f ≫ Quiver.Path.cons g' p = Quiver.Path.cons (f ≫ g') p
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (Quiver.Path.cons (f ≫ g') p) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        (Quiver.Path.cons g' p)
[PROOFSTEP]
simp only at ih ⊢
[GOAL]
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) g'
this : f ≫ Quiver.Path.cons g' p = Quiver.Path.cons (f ≫ g') p
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) (f ≫ g') ≫ φ.map p =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) g' ≫ φ.map p
[PROOFSTEP]
rw [ih, Category.assoc]
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (lift φ).map (Quiver.Hom.toPath f) = φ.map f
[PROOFSTEP]
dsimp [Quiver.Hom.toPath, lift]
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ 𝟙 (φ.obj X) ≫ φ.map f = φ.map f
[PROOFSTEP]
simp
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ of ⋙q (lift φ).toPrefunctor = φ
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ ∀ (X : V), (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X : V
⊢ (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
[PROOFSTEP]
rfl
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of ⋙q (lift φ).toPrefunctor).map f =
      Eq.recOn (_ : φ.obj Y = (of ⋙q (lift φ).toPrefunctor).obj Y)
        (Eq.recOn (_ : φ.obj X = (of ⋙q (lift φ).toPrefunctor).obj X) (φ.map f))
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (of ⋙q (lift φ).toPrefunctor).map f =
    Eq.recOn (_ : φ.obj Y = (of ⋙q (lift φ).toPrefunctor).obj Y)
      (Eq.recOn (_ : φ.obj X = (of ⋙q (lift φ).toPrefunctor).obj X) (φ.map f))
[PROOFSTEP]
rcases φ with ⟨φo, φm⟩
[GOAL]
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ (of ⋙q (lift { obj := φo, map := φm }).toPrefunctor).map f =
    Eq.recOn (_ : { obj := φo, map := φm }.obj Y = (of ⋙q (lift { obj := φo, map := φm }).toPrefunctor).obj Y)
      (Eq.recOn (_ : { obj := φo, map := φm }.obj X = (of ⋙q (lift { obj := φo, map := φm }).toPrefunctor).obj X)
        ({ obj := φo, map := φm }.map f))
[PROOFSTEP]
dsimp [lift, Quiver.Hom.toPath]
[GOAL]
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ 𝟙 (φo X) ≫ φm f = φm f
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
Φ : Paths V ⥤ C
hΦ : of ⋙q Φ.toPrefunctor = φ
⊢ Φ = lift φ
[PROOFSTEP]
subst_vars
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ Φ = lift (of ⋙q Φ.toPrefunctor)
[PROOFSTEP]
fapply Functor.ext
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ ∀ (X : Paths V), Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).obj X
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X : Paths V
⊢ Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).obj X
[PROOFSTEP]
rfl
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam
    (∀ (X Y : Paths V) (f : X ⟶ Y),
      Φ.map f =
        eqToHom (_ : Φ.obj X = Φ.obj X) ≫
          (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom (_ : (lift (of ⋙q Φ.toPrefunctor)).obj Y = Φ.obj Y))
    _auto✝
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
f : X ⟶ Y
⊢ Φ.map f =
    eqToHom (_ : Φ.obj X = Φ.obj X) ≫
      (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom (_ : (lift (of ⋙q Φ.toPrefunctor)).obj Y = Φ.obj Y)
[PROOFSTEP]
dsimp [lift]
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
f : X ⟶ Y
⊢ Φ.map f =
    𝟙 (Φ.obj X) ≫ Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) f ≫ 𝟙 (Φ.obj Y)
[PROOFSTEP]
induction' f with _ _ p f' ih
[GOAL]
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil =
    𝟙 (Φ.obj X) ≫
      Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) Quiver.Path.nil ≫
        𝟙 (Φ.obj X)
[PROOFSTEP]
simp only [Category.comp_id]
[GOAL]
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)
[PROOFSTEP]
apply Functor.map_id
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih :
  Φ.map p =
    𝟙 (Φ.obj X) ≫
      Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p ≫ 𝟙 (Φ.obj b✝)
⊢ Φ.map (Quiver.Path.cons p f') =
    𝟙 (Φ.obj X) ≫
      Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) (Quiver.Path.cons p f') ≫
        𝟙 (Φ.obj c✝)
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp] at ih ⊢
  -- porting note: Had to do substitute `p.cons f'` and `f'.toPath` by their fully qualified
        -- versions in this `have` clause (elsewhere too).
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p
⊢ Φ.map (Quiver.Path.cons p f') =
    Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p ≫
      Φ.map (Quiver.Hom.toPath f')
[PROOFSTEP]
have : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f') := by
  convert Functor.map_comp Φ p (Quiver.Hom.toPath f')
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p
⊢ Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f')
[PROOFSTEP]
convert Functor.map_comp Φ p (Quiver.Hom.toPath f')
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p
this : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f')
⊢ Φ.map (Quiver.Path.cons p f') =
    Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p ≫
      Φ.map (Quiver.Hom.toPath f')
[PROOFSTEP]
rw [this, ih]
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
⊢ F = G
[PROOFSTEP]
fapply Functor.ext
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
⊢ ∀ (X : Paths V), F.obj X = G.obj X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X : Paths V
⊢ F.obj X = G.obj X
[PROOFSTEP]
rw [h_obj]
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
⊢ autoParam
    (∀ (X Y : Paths V) (f : X ⟶ Y),
      F.map f = eqToHom (_ : F.obj X = G.obj X) ≫ G.map f ≫ eqToHom (_ : G.obj Y = F.obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X Y : Paths V
f : X ⟶ Y
⊢ F.map f = eqToHom (_ : F.obj X = G.obj X) ≫ G.map f ≫ eqToHom (_ : G.obj Y = F.obj Y)
[PROOFSTEP]
induction' f with Y' Z' g e ih
[GOAL]
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X Y : Paths V
⊢ F.map Quiver.Path.nil = eqToHom (_ : F.obj X = G.obj X) ≫ G.map Quiver.Path.nil ≫ eqToHom (_ : G.obj X = F.obj X)
[PROOFSTEP]
erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X Y Y' Z' : Paths V
g : Quiver.Path X Y'
e : Y' ⟶ Z'
ih : F.map g = eqToHom (_ : F.obj X = G.obj X) ≫ G.map g ≫ eqToHom (_ : G.obj Y' = F.obj Y')
⊢ F.map (Quiver.Path.cons g e) =
    eqToHom (_ : F.obj X = G.obj X) ≫ G.map (Quiver.Path.cons g e) ≫ eqToHom (_ : G.obj Z' = F.obj Z')
[PROOFSTEP]
erw [F.map_comp g (Quiver.Hom.toPath e), G.map_comp g (Quiver.Hom.toPath e), ih, h]
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X Y Y' Z' : Paths V
g : Quiver.Path X Y'
e : Y' ⟶ Z'
ih : F.map g = eqToHom (_ : F.obj X = G.obj X) ≫ G.map g ≫ eqToHom (_ : G.obj Y' = F.obj Y')
⊢ (eqToHom (_ : F.obj X = G.obj X) ≫ G.map g ≫ eqToHom (_ : G.obj Y' = F.obj Y')) ≫
      eqToHom (_ : F.obj Y' = G.obj Y') ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj Z' = F.obj Z') =
    eqToHom (_ : F.obj X = G.obj X) ≫ (G.map g ≫ G.map (Quiver.Hom.toPath e)) ≫ eqToHom (_ : G.obj Z' = F.obj Z')
[PROOFSTEP]
simp only [Category.id_comp, eqToHom_refl, eqToHom_trans_assoc, Category.assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
g : Path Y Z
⊢ composePath (Path.comp f g) = composePath f ≫ composePath g
[PROOFSTEP]
induction' g with Y' Z' g e ih
[GOAL]
case nil
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
⊢ composePath (Path.comp f Path.nil) = composePath f ≫ composePath Path.nil
[PROOFSTEP]
simp
[GOAL]
case cons
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
Y' Z' : C
g : Path Y Y'
e : Y' ⟶ Z'
ih : composePath (Path.comp f g) = composePath f ≫ composePath g
⊢ composePath (Path.comp f (Path.cons g e)) = composePath f ≫ composePath (Path.cons g e)
[PROOFSTEP]
simp [ih]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ pathsHomRel C (Hom.toPath (𝟙 X))
    (𝟙
      ({ obj := fun X => { as := X },
              map := fun {X Y} f => Quot.mk (Quotient.CompClosure (pathsHomRel C)) (Hom.toPath f) }.obj
          X).as)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ pathsHomRel C (Hom.toPath (f ≫ g)) (Hom.toPath f ≫ Hom.toPath g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
⊢ (𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ (𝟭 (Quotient (pathsHomRel C))).obj { as := as✝ } ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj { as := as✝ }
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Quotient (pathsHomRel C)
f : X✝.as ⟶ Y✝.as
⊢ (𝟭 (Quotient (pathsHomRel C))).map (Quot.mk (Quotient.CompClosure (pathsHomRel C)) f) ≫
      ((fun X =>
            Quotient.casesOn (motive := fun t =>
              X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
              (fun as h => (_ : { as := as } = X) ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as }))
              (_ : X = X))
          Y✝).hom =
    ((fun X =>
            Quotient.casesOn (motive := fun t =>
              X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
              (fun as h => (_ : { as := as } = X) ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as }))
              (_ : X = X))
          X✝).hom ≫
      (quotientPathsTo C ⋙ toQuotientPaths C).map (Quot.mk (Quotient.CompClosure (pathsHomRel C)) f)
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Quotient (pathsHomRel C)
f : X✝.as ⟶ Y✝.as
⊢ Quotient.CompClosure (pathsHomRel C) (f ≫ 𝟙 ((𝟭 (Quotient (pathsHomRel C))).obj { as := Y✝.as }).as)
    (𝟙 ((𝟭 (Quotient (pathsHomRel C))).obj { as := X✝.as }).as ≫
      Hom.toPath ((quotientPathsTo C).map (Quot.mk (Quotient.CompClosure (pathsHomRel C)) f)))
[PROOFSTEP]
apply Quotient.CompClosure.of
[GOAL]
case a.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Quotient (pathsHomRel C)
f : X✝.as ⟶ Y✝.as
⊢ pathsHomRel C (f ≫ 𝟙 ((𝟭 (Quotient (pathsHomRel C))).obj { as := Y✝.as }).as)
    (𝟙 ((𝟭 (Quotient (pathsHomRel C))).obj { as := X✝.as }).as ≫
      Hom.toPath ((quotientPathsTo C).map (Quot.mk (Quotient.CompClosure (pathsHomRel C)) f)))
[PROOFSTEP]
simp [Category.comp_id, Category.id_comp, pathsHomRel]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (toQuotientPaths C ⋙ quotientPathsTo C).map f ≫
      ((fun X => Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj X)) Y✝).hom =
    ((fun X => Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj X)) X✝).hom ≫ (𝟭 C).map f
[PROOFSTEP]
simp [Quot.liftOn_mk]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
⊢ (quotientPathsTo C).map
        (NatTrans.app
          (NatIso.ofComponents fun X =>
              Quotient.casesOn (motive := fun t =>
                X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
                (fun as h => (_ : { as := as } = X) ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as }))
                (_ : X = X)).hom
          X) ≫
      NatTrans.app (NatIso.ofComponents fun X => Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj X)).hom
        ((quotientPathsTo C).obj X) =
    𝟙 ((quotientPathsTo C).obj X)
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ (quotientPathsTo C).map
        (NatTrans.app
          (NatIso.ofComponents fun X =>
              Quotient.casesOn (motive := fun t =>
                X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
                (fun as h => (_ : { as := as } = X) ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as }))
                (_ : X = X)).hom
          { as := as✝ }) ≫
      NatTrans.app (NatIso.ofComponents fun X => Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj X)).hom
        ((quotientPathsTo C).obj { as := as✝ }) =
    𝟙 ((quotientPathsTo C).obj { as := as✝ })
[PROOFSTEP]
simp only [pathsHomRel, pathComposition_obj, pathComposition_map, Functor.id_obj, quotientPathsTo_obj, Functor.comp_obj,
  toQuotientPaths_obj_as, NatIso.ofComponents_hom_app, Iso.refl_hom, quotientPathsTo_map, Category.comp_id]
[GOAL]
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ Quot.liftOn (𝟙 { as := as✝ }) (fun f => composePath f)
      (_ :
        ∀ (a b : { as := as✝ }.as ⟶ ((toQuotientPaths C).obj as✝).as),
          Quotient.CompClosure (fun x x_1 p q => composePath p = composePath q) a b →
            (fun f => composePath f) a = (fun f => composePath f) b) =
    𝟙 as✝
[PROOFSTEP]
rfl
