Theorem: SimpleGraph.push_eq_nil (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
x y : V
f : V → V'
w : V'
p : Walk G x y
hp : ∀ z ∈ Walk.support p, f z = w
⊢ Walk.Nil (push_Walk f p)
Tactic:
simp [tata.mp <| push_eq_nil' hp]
State after:
no goals