no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w : V
inst✝ : DecidableEq V
c : Walk G v v
h : u ∈ support c
⊢ Walk.toSubgraph (rotate c h) = Walk.toSubgraph c
rw [rotate, toSubgraph_append, sup_comm, ← toSubgraph_append, take_spec]