Theorem: SimpleGraph.Walk.tail₀_cons (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
e : Adj G c a
⊢ tail₀ (cons e p) = support p
Tactic:
induction p generalizing c with
| nil => rfl
| cons h p ih => simpa [tail₀] using ih (e := h)
State after:
no goals

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

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