list_take_join into mathlib

Stream: general

[Martin Dvořák]

Patrick Johnson provided me with this beautiful piece of code:
https://github.com/user7230724/lean-projects/blob/master/src/list_take_join/main.lean

I wanted to PR it into mathlib (together with analogues lemmata for list.drop I was going to write). I should have asked first, however, whether you want it in mathlib. Would you require the lemmata to be more constructive? Or is it OK for mathlib as Patrick Johnson wrote them?

[Eric Wieser]

I think this is the type of thing that is easiest to just discuss in review where we can comment on individual lines

[Martin Dvořák]

I was going to. But first, I want to make sure it is desired at all.

[Eric Wieser]

Personally I don't like the statement of the final result, but many of the intermediate results look great

[Martin Dvořák]

Can I get a preliminary feedback please?
https://github.com/leanprover-community/mathlib/pull/17190
I don't know whether the contribution is going in the right direction.

[Martin Dvořák]

In the end, I kept only the intermediate results in the PR.