α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
n : ℕ
hn : n < length (cyclicPermutations (rotate l k))
hn' : n < length (rotate (cyclicPermutations l) k)
⊢ nthLe (cyclicPermutations (rotate l k)) n hn = nthLe (rotate (cyclicPermutations l) k) n hn'
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
⊢ cyclicPermutations (rotate l k) = rotate (cyclicPermutations l) k
refine' ext_nthLe this fun n hn hn' => _
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
n : ℕ
hn : n < length (cyclicPermutations (rotate l k))
hn' : n < length (rotate (cyclicPermutations l) k)
⊢ rotate l ((n + k) % length l) =
    nthLe (cyclicPermutations l) ((n + k) % length (cyclicPermutations l))
      (_ : (n + k) % length (cyclicPermutations l) < length (cyclicPermutations l))
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
n : ℕ
hn : n < length (cyclicPermutations (rotate l k))
hn' : n < length (rotate (cyclicPermutations l) k)
⊢ nthLe (cyclicPermutations (rotate l k)) n hn = nthLe (rotate (cyclicPermutations l) k) n hn'
rw [nthLe_rotate, nthLe_cyclicPermutations, rotate_rotate, ← rotate_mod, add_comm]
no goals
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
n : ℕ
hn : n < length (cyclicPermutations (rotate l k))
hn' : n < length (rotate (cyclicPermutations l) k)
⊢ rotate l ((n + k) % length l) =
    nthLe (cyclicPermutations l) ((n + k) % length (cyclicPermutations l))
      (_ : (n + k) % length (cyclicPermutations l) < length (cyclicPermutations l))
cases l <;> simp
case nil
α : Type u
l l' : List α
k : ℕ
⊢ length (cyclicPermutations (rotate [] k)) = length (rotate (cyclicPermutations []) k)

case cons
α : Type u
l l' : List α
k : ℕ
head✝ : α
tail✝ : List α
⊢ length (cyclicPermutations (rotate (head✝ :: tail✝) k)) = length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
α : Type u
l✝ l' l : List α
k : ℕ
⊢ length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
cases l
no goals
case nil
α : Type u
l l' : List α
k : ℕ
⊢ length (cyclicPermutations (rotate [] k)) = length (rotate (cyclicPermutations []) k)
simp
no goals
case cons
α : Type u
l l' : List α
k : ℕ
head✝ : α
tail✝ : List α
⊢ length (cyclicPermutations (rotate (head✝ :: tail✝) k)) = length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
rw [length_cyclicPermutations_of_ne_nil] <;> simp