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

case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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))
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
φ : V ⥤q C
⊢ of ⋙q (lift φ).toPrefunctor = φ
fapply Prefunctor.ext
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
φ : V ⥤q C
X : V
⊢ (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
φ : V ⥤q C
⊢ ∀ (X : V), (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
rintro X
no goals
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
φ : V ⥤q C
X : V
⊢ (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
rfl
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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))
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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))
rintro X Y f
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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))
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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))
rcases φ with ⟨φo, φm⟩
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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))
dsimp [lift, Quiver.Hom.toPath]
no goals
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category 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
simp only [Category.id_comp]