α : Type u
l✝ l' l : List α
x : α
h : cyclicPermutations l = [[x]]
⊢ l = [x]
α : Type u
l✝ l' l : List α
x : α
⊢ cyclicPermutations l = [[x]] ↔ l = [x]
refine' ⟨fun h => _, fun h => by simp [cyclicPermutations, h, dropLast_eq_take]⟩
no goals
α : Type u
l✝ l' l : List α
x : α
h : cyclicPermutations l = [[x]]
⊢ l = [x]
rw [eq_comm, ← isRotated_singleton_iff', ← mem_cyclicPermutations_iff, h, mem_singleton]
no goals
α : Type u
l✝ l' l : List α
x : α
h : l = [x]
⊢ cyclicPermutations l = [[x]]
simp [cyclicPermutations, h, dropLast_eq_take]