Theorem: Graph.toList_cast_terminal (GroupComp/Graph/ReducedPaths.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w w' : V
p : EdgePath G v w
eqn : w = w'
⊢ toList p = toList (eqn ▸ p)
Tactic:
cases eqn
State after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
⊢ toList p = toList ((_ : w = w) ▸ p)

State before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
⊢ toList p = toList ((_ : w = w) ▸ p)
Tactic:
rfl
State after:
no goals