V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
Φ : Paths V ⥤ C
⊢ Φ = lift (of ⋙q Φ.toPrefunctor)
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
φ : V ⥤q C
Φ : Paths V ⥤ C
hΦ : of ⋙q Φ.toPrefunctor = φ
⊢ Φ = lift φ
subst_vars
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
Φ : Paths V ⥤ C
⊢ ∀ (X : Paths V), Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).obj X

case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
Φ : Paths V ⥤ C
⊢ autoParam
    (∀ (X Y : Paths V) (f : X ⟶ Y),
      Φ.map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom (_ : (lift (of ⋙q Φ.toPrefunctor)).obj Y = Φ.obj Y))
    _auto✝
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
Φ : Paths V ⥤ C
⊢ Φ = lift (of ⋙q Φ.toPrefunctor)
fapply Functor.ext
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
Φ : Paths V ⥤ C
X : Paths V
⊢ Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).obj X
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
Φ : Paths V ⥤ C
⊢ ∀ (X : Paths V), Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).obj X
rintro X
no goals
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
Φ : Paths V ⥤ C
X : Paths V
⊢ Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).obj X
rfl
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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)
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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✝
rintro X Y f
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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)
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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)
dsimp [lift]
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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)

case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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✝)
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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)
induction' f with _ _ p f' ih
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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)
simp only [Category.comp_id]
no goals
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)
apply Functor.map_id
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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')
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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✝)
simp only [Category.comp_id, Category.id_comp] at ih ⊢
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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')
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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')
have : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f') := by
  convert Functor.map_comp Φ p (Quiver.Hom.toPath f')
no goals
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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')
rw [this, ih]
no goals
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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')
convert Functor.map_comp Φ p (Quiver.Hom.toPath f')