Theorem: Graph.liftTerminal_of_proj (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₁ w₁ : V₁
e : EdgePath G₁ v₁ w₁
⊢ liftTerminal p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e p) = w₁
Tactic:
simp only [liftTerminal, liftClass, lift_of_proj]
State after:
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 : EdgePath G₁ v₁ w₁
⊢ (PathLift.pathClass
        { τ := w₁, path := e, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e) = toList (EdgePath.map e p)) }).τ =
    w₁

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₁ w₁ : V₁
e : EdgePath G₁ v₁ w₁
⊢ (PathLift.pathClass
        { τ := w₁, path := e, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e) = toList (EdgePath.map e p)) }).τ =
    w₁
Tactic:
rfl
State after:
no goals