English
For any l, n, k and hk: k < length(l), the k-th element of l equals the element of l.rotate n at index (length(l) - (n mod length(l)) + k) mod length(l).
Русский
Для любого l, n, k и hk: k < длина(l), элемент на позиции k в l равен элементу l.rotate n на позиции (длина(l) - (n mod длина(l)) + k) mod длина(l).
LaTeX
$$$\\forall {\alpha} (l:\\List\\alpha) (n:\\mathbb{N}) (k:\\mathbb{N}) (hk:\\ k < |l|), \\ l[k] = (l.rotate n)[( |l| - n \\% |l| + k) \\% |l|]$$$
Lean4
/-- A version of `List.getElem_rotate` that represents `l[k]` in terms of
`(List.rotate l n)[⋯]`, not vice versa. Can be used instead of rewriting `List.getElem_rotate`
from right to left. -/
theorem getElem_eq_getElem_rotate (l : List α) (n : ℕ) (k : Nat) (hk : k < l.length) :
l[k] =
((l.rotate
n)[(l.length - n % l.length + k) %
l.length]'((Nat.mod_lt _ (k.zero_le.trans_lt hk)).trans_eq (length_rotate _ _).symm)) :=
by
rw [getElem_rotate]
refine congr_arg l.get (Fin.eq_of_val_eq ?_)
simp only [mod_add_mod]
rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]
exacts [hk, (mod_lt _ (k.zero_le.trans_lt hk)).le]
