Theorem: SimpleGraph.Walk.init_eq_take_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
⊢ init₀ p = init (support p)
Tactic:
induction p with
| nil => rfl
| cons _ _ ih => simp [ih, _root_.List.init]
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
⊢ init₀ nil = init (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 : init₀ p✝ = init (support p✝)
⊢ init₀ (cons h✝ p✝) = init (support (cons h✝ p✝))
Tactic:
simp [ih, _root_.List.init]
State after:
no goals