α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ ↑(cyclicPermutations l) ↔ ↑l✝ = Quotient.mk'' l
α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ lists (Quotient.mk'' l) ↔ ↑l✝ = Quotient.mk'' l
rw [lists, Quotient.liftOn'_mk'']
no goals
α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ ↑(cyclicPermutations l) ↔ ↑l✝ = Quotient.mk'' l
simp