no goals
α : Type u
x✝ : α
n : ℕ
⊢ x✝ ∈ rotate [] n ↔ x✝ ∈ []
simp
no goals
α : Type u
a : α
l : List α
x✝ : α
⊢ x✝ ∈ rotate (a :: l) 0 ↔ x✝ ∈ a :: l
simp
no goals
α : Type u
a : α
l : List α
x✝ : α
n : ℕ
⊢ x✝ ∈ rotate (a :: l) (n + 1) ↔ x✝ ∈ a :: l
simp [rotate_cons_succ, mem_rotate, or_comm]