Theorem: Graph.UniversalCover.reduced_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
p : EdgePath G x₀ τ
hyp : reduced p
⊢ liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p =
    { τ := τ, p := p, is_reduced := hyp }
Tactic:
simp [liftTerminal, liftClass, lift_of_reduced p hyp, rayLift]
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
p : EdgePath G x₀ τ
hyp : reduced p
⊢ (PathLift.pathClass
        { τ := { τ := τ, p := p, is_reduced := hyp }, path := rayTo G x₀ τ p hyp,
          term_pushdown :=
            (_ :
              (proj G x₀).toFuncV { τ := τ, p := p, is_reduced := hyp } =
                (proj G x₀).toFuncV { τ := τ, p := p, is_reduced := hyp }),
          list_pushdown :=
            (_ : List.map (proj G x₀).toFuncE (EdgePath.toList (rayTo G x₀ τ p hyp)) = EdgePath.toList p) }).τ =
    { τ := τ, p := p, is_reduced := hyp }

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
p : EdgePath G x₀ τ
hyp : reduced p
⊢ (PathLift.pathClass
        { τ := { τ := τ, p := p, is_reduced := hyp }, path := rayTo G x₀ τ p hyp,
          term_pushdown :=
            (_ :
              (proj G x₀).toFuncV { τ := τ, p := p, is_reduced := hyp } =
                (proj G x₀).toFuncV { τ := τ, p := p, is_reduced := hyp }),
          list_pushdown :=
            (_ : List.map (proj G x₀).toFuncE (EdgePath.toList (rayTo G x₀ τ p hyp)) = EdgePath.toList p) }).τ =
    { τ := τ, p := p, is_reduced := hyp }
Tactic:
rfl
State after:
no goals