case inl
α : Type u
l l' : List α
n : ℕ
hn : n < length (cyclicPermutations [])
⊢ nthLe (cyclicPermutations []) n hn = rotate [] n

case inr
α : Type u
l✝ l' l : List α
n : ℕ
hn : n < length (cyclicPermutations l)
h : l ≠ []
⊢ nthLe (cyclicPermutations l) n hn = rotate l n
α : Type u
l✝ l' l : List α
n : ℕ
hn : n < length (cyclicPermutations l)
⊢ nthLe (cyclicPermutations l) n hn = rotate l n
obtain rfl | h := eq_or_ne l []
no goals
case inl
α : Type u
l l' : List α
n : ℕ
hn : n < length (cyclicPermutations [])
⊢ nthLe (cyclicPermutations []) n hn = rotate [] n
simp
case inr
α : Type u
l✝ l' l : List α
n : ℕ
hn✝ : n < length (cyclicPermutations l)
hn : n < length l
h : l ≠ []
⊢ nthLe (cyclicPermutations l) n hn✝ = rotate l n
case inr
α : Type u
l✝ l' l : List α
n : ℕ
hn : n < length (cyclicPermutations l)
h : l ≠ []
⊢ nthLe (cyclicPermutations l) n hn = rotate l n
rw [length_cyclicPermutations_of_ne_nil _ h] at hn
no goals
case inr
α : Type u
l✝ l' l : List α
n : ℕ
hn✝ : n < length (cyclicPermutations l)
hn : n < length l
h : l ≠ []
⊢ nthLe (cyclicPermutations l) n hn✝ = rotate l n
simp [dropLast_eq_take, cyclicPermutations_of_ne_nil _ h, nthLe_take',
  rotate_eq_drop_append_take hn.le]