English
If a list l is a chain with respect to the relation defined by f x = y, then the i-th element of l is obtained by applying f i times to the first element. More precisely, if l satisfies that successive elements relate by f x = y, then the i-th element equals f applied i times to the first element.
Русский
Если список l является цепью для отношения, заданного равенством f x = y между соседними элементами, то i-й элемент равен применению f i раз к первому элементу списка.
LaTeX
$$$\\forall \\alpha f:\\alpha\\to\\alpha,\\ l:\\text{List }\\alpha,\\ hl: List.IsChain (\\lambda x y . f\\,x = y)\\ l\\Rightarrow\\ \\forall i:\\mathbb{N},\\ (i<|l|)\\Rightarrow f^{i}(l_0) = l_i$$$
Lean4
theorem iterate_eq_of_apply_eq {α : Type*} {f : α → α} {l : List α} (hl : l.IsChain (fun x y ↦ f x = y)) (i : ℕ)
(hi : i < l.length) : f^[i] l[0] = l[i] := by
induction i with
| zero => rfl
| succ i h =>
rw [Function.iterate_succ', Function.comp_apply, h (by cutsat)]
rw [List.isChain_iff_get] at hl
apply hl
