Theorem: Graph.UniversalCover.proj_liftTerminal (GroupComp/Graph/UniversalCover.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ : V
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e (proj G x₀)) =
    vert
Tactic:
simp [liftTerminal, liftClass]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ : V
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ (PathLift.pathClass
        (lift (EdgePath.map e (proj G x₀)) (proj G x₀) (basepoint G x₀)
          (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)))).τ =
    vert

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ : V
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ (PathLift.pathClass
        (lift (EdgePath.map e (proj G x₀)) (proj G x₀) (basepoint G x₀)
          (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)))).τ =
    vert
Tactic:
simp [lift_of_proj]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ : V
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ (PathLift.pathClass
        { τ := vert, path := e, term_pushdown := (_ : (proj G x₀).toFuncV vert = (proj G x₀).toFuncV vert),
          list_pushdown :=
            (_ : List.map (proj G x₀).toFuncE (EdgePath.toList e) = EdgePath.toList (EdgePath.map e (proj G x₀))) }).τ =
    vert

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ : V
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ (PathLift.pathClass
        { τ := vert, path := e, term_pushdown := (_ : (proj G x₀).toFuncV vert = (proj G x₀).toFuncV vert),
          list_pushdown :=
            (_ : List.map (proj G x₀).toFuncE (EdgePath.toList e) = EdgePath.toList (EdgePath.map e (proj G x₀))) }).τ =
    vert
Tactic:
rfl
State after:
no goals