feat(data/list): more lemmas on joins and sums (#2501)
A few more lemmas on lists (especially joins) and sums. I also linted the file `lists/basic.lean` and converted some comments to section headers.
Some lemmas got renamed:
`of_fn_prod_take` -> `prod_take_of_fn`
`of_fn_sum_take` -> `sum_take_of_fn`
`of_fn_prod` ->`prod_of_fn`
`of_fn_sum` -> `sum_of_fn`
The arguments of `nth_le_repeat` were changed for better `simp` efficiency
