Theorem: Graph.toList_cast_init (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 v' w : V
p : EdgePath G v w
eqn : v = v'
⊢ 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 v' w : V
p✝ : EdgePath G v w
eqn : v = v'
p : EdgePath G v w
⊢ toList p = toList ((_ : v = v) ▸ p)
Tactic:
rfl
State after:
no goals