Theorem: Graph.PathLift.toFuncV_init (Lectures/Graph.lean)

State before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : CoveringMap G₁ G₂
v₁ : V₁
v₂ w₂ : V₂
h : p.toMorphism.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
lift : PathLift p v₁ v₂ w₂ h e
⊢ Morphism.pathMap p.toMorphism v₁ lift.w₁ lift.path v₂ w₂ h (_ : p.toMorphism.toFuncV lift.w₁ = w₂) = e
Tactic:
apply eq_of_toList_eq
State after:
case a
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : CoveringMap G₁ G₂
v₁ : V₁
v₂ w₂ : V₂
h : p.toMorphism.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
lift : PathLift p v₁ v₂ w₂ h e
⊢ toList (Morphism.pathMap p.toMorphism v₁ lift.w₁ lift.path v₂ w₂ h (_ : p.toMorphism.toFuncV lift.w₁ = w₂)) = toList e

State before:
case a
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : CoveringMap G₁ G₂
v₁ : V₁
v₂ w₂ : V₂
h : p.toMorphism.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
lift : PathLift p v₁ v₂ w₂ h e
⊢ toList (Morphism.pathMap p.toMorphism v₁ lift.w₁ lift.path v₂ w₂ h (_ : p.toMorphism.toFuncV lift.w₁ = w₂)) = toList e
Tactic:
rw [pathMap_toList, lift.list_pushdown]
State after:
no goals