English
For any f: Γ → Γ, any n, i, and ListBlank L, the nth element of L.modifyNth f n is f(L.nth i) if i = n, otherwise L.nth i.
Русский
Для любой f: Γ → Γ, любого n и i, для ListBlank L, элемент на месте i после L.modifyNth f n равен f(L.nth i) если i = n, иначе L.nth i.
LaTeX
$$$\forall {\Gamma} [Inhabited(\Gamma)]\,(f : \Gamma → \Gamma)\ (n i : \mathbb{N})\ (L : ListBlank(\Gamma)):\ (L.modifyNth f n).nth i = \text{if } i = n \text{ then } f(L.nth i) \text{ else } L.nth i$$$
Lean4
theorem nth_modifyNth {Γ} [Inhabited Γ] (f : Γ → Γ) (n i) (L : ListBlank Γ) :
(L.modifyNth f n).nth i = if i = n then f (L.nth i) else L.nth i := by
induction n generalizing i L with
| zero =>
cases i <;>
simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.nth_succ, if_false,
ListBlank.tail_cons, reduceCtorEq]
| succ n IH =>
cases i
· rw [if_neg (Nat.succ_ne_zero _).symm]
simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth]
· simp only [IH, ListBlank.modifyNth, ListBlank.nth_succ, ListBlank.tail_cons, Nat.succ.injEq]
