English
Let l be a finite list, and let i be a natural number with i < length(l). Then the list formed by taking the first i elements of l and appending the i-th element of l equals the first i+1 elements of l, i.e. take i l ++ [l[i]] = take (i+1) l.
Русский
Пусть l — конечный список, и пусть i — натуральное число такое, что i < длина(l). Тогда список, состоящий из первых i элементов списка l, дополненный i-ым элементом l, равен первому i+1 элементам l: take i l ++ [l[i]] = take (i+1) l.
LaTeX
$$$\\mathrm{length}(\\mathrm{takeI}(n, l)) = n$$$
Lean4
/-- `take_concat_get` in simp normal form -/
theorem take_concat_get' (l : List α) (i : ℕ) (h : i < l.length) : l.take i ++ [l[i]] = l.take (i + 1) := by simp
