English
Taking the flatten of the first i sublists and then taking the sum of their lengths equals taking the flatten of the first i sublists directly.
Русский
Вырезание плоского списка через суммарную длину первых i подсписков эквивалентно взятию плоского списка первых i подсписков.
LaTeX
$$$L.flatten.take ((L.map length).take i).sum = (L.take i).flatten$$
Lean4
/-- In a flatten, taking the first elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the flatten of the first `i` sublists. -/
theorem take_sum_flatten (L : List (List α)) (i : ℕ) :
L.flatten.take ((L.map length).take i).sum = (L.take i).flatten :=
by
induction L generalizing i
· simp
· cases i <;> simp [take_length_add_append, *]
