Theorem: Digraph.Walk.support_rotate (GraphProjects/DigraphConnectivity.lean)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph 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)
Tactic:
simp only [rotate, tail_support_append]
State after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph 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)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph 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)
Tactic:
apply List.IsRotated.trans List.isRotated_append
State after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph 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)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph 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)
Tactic:
rw [← tail_support_append, take_spec]
State after:
no goals