Theorem: SimpleGraph.Walk.support_eq_init₀_union_last (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 = init₀ p ++ [b]
Tactic:
induction p with
| nil => rfl
| cons _ p ih => simp [ih]
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 = init₀ nil ++ [u✝]
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 = init₀ p ++ [w✝]
⊢ support (cons h✝ p) = init₀ (cons h✝ p) ++ [w✝]
Tactic:
simp [ih]
State after:
no goals