Theorem: SimpleGraph.Walk.tail_eq_tail_support (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
⊢ tail₀ p = List.tail (support p)
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
⊢ tail₀ nil = List.tail (support 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 : tail₀ p = List.tail (support p)
⊢ tail₀ (cons h✝ p) = List.tail (support (cons h✝ p))
Tactic:
simp [ih]
State after:
no goals