Theorem: SimpleGraph.Walk.support_eq_head_union_tail₀ (Untitled/Graphs/Walk.lean)

State before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
⊢ support p = a :: tail₀ p
Tactic:
induction p with
| nil => rfl
| cons _ p ih => simp [ih, Walk.tail₀]
State after:
no goals

State before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
⊢ support nil = u✝ :: tail₀ nil
Tactic:
rfl
State after:
no goals

State before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : support p = v✝ :: tail₀ p
⊢ support (cons h✝ p) = u✝ :: tail₀ (cons h✝ p)
Tactic:
simp [ih, Walk.tail₀]
State after:
no goals