English
If n ≤ length(l), then l.rotate' n = l.drop n ++ l.take n.
Русский
Если n ≤ длина(l), то l.rotate' n = l.drop n ++ l.take n.
LaTeX
$$$\\forall \\alpha \\in \\mathsf{Type},\\ \\forall l \\in \\mathsf{List}(\\alpha),\\forall n \\in \\mathbb{N},\\ n \\leq \\operatorname{length}(l)\\ \\Rightarrow\\ l.rotate' n = l.drop n ++ l.take n$$$
Lean4
theorem rotate'_eq_drop_append_take : ∀ {l : List α} {n : ℕ}, n ≤ l.length → l.rotate' n = l.drop n ++ l.take n
| [], n, h => by simp
| l, 0, h => by simp
| a :: l, n + 1, h => by
have hnl : n ≤ l.length := le_of_succ_le_succ h
have hnl' : n ≤ (l ++ [a]).length := by rw [length_append, length_cons, List.length]; exact le_of_succ_le h
rw [rotate'_cons_succ, rotate'_eq_drop_append_take hnl', drop, take, drop_append_of_le_length hnl,
take_append_of_le_length hnl];
simp
