case nil
α : Type u
l l' : List α
⊢ [] ∈ cyclicPermutations []

case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ x :: l ∈ cyclicPermutations (x :: l)
α : Type u
l✝ l' l : List α
⊢ l ∈ cyclicPermutations l
cases' l with x l
no goals
case nil
α : Type u
l l' : List α
⊢ [] ∈ cyclicPermutations []
simp
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ ∃ n h, nthLe (cyclicPermutations (x :: l)) n h = x :: l
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ x :: l ∈ cyclicPermutations (x :: l)
rw [mem_iff_nthLe]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ nthLe (cyclicPermutations (x :: l)) 0 (_ : 0 < length (cyclicPermutations (x :: l))) = x :: l
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ ∃ n h, nthLe (cyclicPermutations (x :: l)) n h = x :: l
refine' ⟨0, by simp, _⟩
no goals
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ nthLe (cyclicPermutations (x :: l)) 0 (_ : 0 < length (cyclicPermutations (x :: l))) = x :: l
simp
no goals
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ 0 < length (cyclicPermutations (x :: l))
simp