English
An element a appears in l.rotate n if and only if it appears in l.
Русский
Элемент a встречается в l.rotate n тогда и только тогда, когда он встречается в l.
LaTeX
$$$\\forall \\alpha \\in \\mathsf{Type},\\forall l \\in \\mathsf{List}(\\alpha),\\forall a \\in \\alpha,\\ (a \\in l.rotate n) \\Leftrightarrow (a \\in l)$$$
Lean4
@[simp]
theorem mem_rotate : ∀ {l : List α} {a : α} {n : ℕ}, a ∈ l.rotate n ↔ a ∈ l
| [], _, n => by simp
| a :: l, _, 0 => by simp
| a :: l, _, n + 1 => by simp [rotate_cons_succ, mem_rotate, or_comm]