Theorem: Graph.EdgePath.lift_append (GroupComp/Graph/Covering.lean)

State before:
V : Type u
E : Type v
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 : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ u₂ : V₂
h : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
e' : EdgePath G₂ w₂ u₂
⊢ lift (e ++ e') p v₁ h =
    PathLift.append (lift e p v₁ h) (lift e' p (lift e p v₁ h).τ (_ : p.toFuncV (lift e p v₁ h).τ = w₂))
Tactic:
apply unique_Pathlift
State after:
no goals