case intro.intro
α : Type u
l✝ l : List α
k : ℕ
hk : k < length (cyclicPermutations l)
h : nthLe (cyclicPermutations l) k hk ∈ cyclicPermutations l
⊢ length (nthLe (cyclicPermutations l) k hk) = length l
α : Type u
l✝ l' l : List α
h : l' ∈ cyclicPermutations l
⊢ length l' = length l
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem h
no goals
case intro.intro
α : Type u
l✝ l : List α
k : ℕ
hk : k < length (cyclicPermutations l)
h : nthLe (cyclicPermutations l) k hk ∈ cyclicPermutations l
⊢ length (nthLe (cyclicPermutations l) k hk) = length l
simp