rw [lift_of_proj] at lem
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  (lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq [[(lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  { τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq
      [[{ τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]