case h_obj
U : Type ?u.7420
V : Type u_2
W : Type ?u.7426
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X

case h_map
U : Type ?u.7420
V : Type u_2
W : Type ?u.7426
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of ⋙q lift φ).map f =
      Eq.recOn (_ : φ.obj Y = (of ⋙q lift φ).obj Y) (Eq.recOn (_ : φ.obj X = (of ⋙q lift φ).obj X) (φ.map f))
U : Type ?u.7420
V : Type u_2
W : Type ?u.7426
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ of ⋙q lift φ = φ
fapply Prefunctor.ext
case h_obj
U : Type ?u.7420
V : Type u_2
W : Type ?u.7426
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X : V
⊢ (of ⋙q lift φ).obj X = φ.obj X
case h_obj
U : Type ?u.7420
V : Type u_2
W : Type ?u.7426
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X
rintro X
no goals
case h_obj
U : Type ?u.7420
V : Type u_2
W : Type ?u.7426
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X : V
⊢ (of ⋙q lift φ).obj X = φ.obj X
rfl
case h_map
U : Type ?u.7420
V : Type u_2
W : Type ?u.7426
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X Y : V
f : X ⟶ Y
⊢ (of ⋙q lift φ).map f =
    Eq.recOn (_ : φ.obj Y = (of ⋙q lift φ).obj Y) (Eq.recOn (_ : φ.obj X = (of ⋙q lift φ).obj X) (φ.map f))
case h_map
U : Type ?u.7420
V : Type u_2
W : Type ?u.7426
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of ⋙q lift φ).map f =
      Eq.recOn (_ : φ.obj Y = (of ⋙q lift φ).obj Y) (Eq.recOn (_ : φ.obj X = (of ⋙q lift φ).obj X) (φ.map f))
rintro X Y f
no goals
case h_map
U : Type ?u.7420
V : Type u_2
W : Type ?u.7426
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X Y : V
f : X ⟶ Y
⊢ (of ⋙q lift φ).map f =
    Eq.recOn (_ : φ.obj Y = (of ⋙q lift φ).obj Y) (Eq.recOn (_ : φ.obj X = (of ⋙q lift φ).obj X) (φ.map f))
rfl