English
For any l, n and k with hk: k < length(l), l.get k equals the rotated list's get at a corresponding Fin index, namely the index ((length(l) - n mod length(l) + k) mod length(l)) in l.rotate n.
Русский
Для любого списка l, n и k с hk: k < длина(l), l.get k равно get у (l.rotate n) по соответствующему индексу Fin, равному ((длина(l) - (n mod длина(l)) + k) mod длина(l)).
LaTeX
$$$\\forall {l:\\mathrm{List}\\alpha} (n:\\mathbb{N}) (k:\\mathbb{N}) (hk:\\ k < |l|), \\ l.get k = (l.rotate n).get \\langle (|l| - n \\% |l| + k) \\% |l|, \\rangle$$$
Lean4
/-- A version of `List.get_rotate` that represents `List.get l` in terms of
`List.get (List.rotate l n)`, not vice versa. Can be used instead of rewriting `List.get_rotate`
from right to left. -/
theorem get_eq_get_rotate (l : List α) (n : ℕ) (k : Fin l.length) :
l.get k =
(l.rotate n).get
⟨(l.length - n % l.length + k) % l.length,
(Nat.mod_lt _ (k.1.zero_le.trans_lt k.2)).trans_eq (length_rotate _ _).symm⟩ :=
by
rw [get_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 [k.2, (mod_lt _ (k.1.zero_le.trans_lt k.2)).le]
