V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v : V
c : Walk G v v
h : u ∈ support c
⊢ (List.tail (support (dropUntil c u h)) ++ List.tail (support (takeUntil c u h))) ~r List.tail (support c)
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v : V
c : Walk G v v
h : u ∈ support c
⊢ List.tail (support (rotate c h)) ~r List.tail (support c)
simp only [rotate, tail_support_append]
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v : V
c : Walk G v v
h : u ∈ support c
⊢ (List.tail (support (takeUntil c u h)) ++ List.tail (support (dropUntil c u h))) ~r List.tail (support c)
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v : V
c : Walk G v v
h : u ∈ support c
⊢ (List.tail (support (dropUntil c u h)) ++ List.tail (support (takeUntil c u h))) ~r List.tail (support c)
apply List.IsRotated.trans List.isRotated_append
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v : V
c : Walk G v v
h : u ∈ support c
⊢ (List.tail (support (takeUntil c u h)) ++ List.tail (support (dropUntil c u h))) ~r List.tail (support c)
rw [← tail_support_append, take_spec]