English
Let L be a list of finite lists and i a natural number. Dropping the first sum of lengths of the first i sublists from the flattened list is the same as flattening the list after dropping the first i sublists.
Русский
Пусть L — список конечных списков, и i — естественное число. Опуская первые суммы длин первых i подсписков в плоском списке, получаем тот же результат, что и после расплющивания списка после пропуска первых i подсписков.
LaTeX
$$$\\\\forall L \colon \\\\text{List}(\\\\text{List } \\\\\\alpha), \\\\forall i \\\\in \\\\mathbb{N}, \\\\text{flatten}(L).\\\\text{drop}( (L\\\\text{.map length}).\\\\text{take } i).\\\\text{sum} \\\\equiv \\\\text{(drop } i \\\\, L).\\\\text{flatten}$$$
Lean4
/-- In a flatten, dropping all the elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the join after dropping the first `i` sublists. -/
theorem drop_sum_flatten (L : List (List α)) (i : ℕ) :
L.flatten.drop ((L.map length).take i).sum = (L.drop i).flatten :=
by
induction L generalizing i
· simp
· cases i <;> simp [*]
