Theorem: Graph.toList_cast_terminal (Lectures/Graph.lean)

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' : V
p : EdgePath G v w
eqn : w = w'
⊢ toList p = toList (eqn ▸ p)
Tactic:
match p, eqn with
| p, rfl => rfl
State after:
no goals

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' : V
p✝ : EdgePath G v w
eqn : w = w'
p : EdgePath G v w
⊢ toList p = toList ((_ : w = w) ▸ p)
Tactic:
rfl
State after:
no goals