chore(Data/List/Basic): split take and drop from file

[BoltonBailey]

This PR splits Data/List/Basic.lean decls and lemmas related to take or drop into a new TakeDrop.lean file, decreasing the length of a file triggering the long file linter.

---

[github-actions]

PR summary 848261948d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Array.Lemmas	366	362	-4 (-1.09%)

Import changes for all files

Files	Import difference
There are 4102 files with changed transitive imports taking up over 178422 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ splitAt_eq_take_drop

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Vierkantor]

Nice work overall, the split makes sense although it's unfortunate it only ends up reducing the total number of lines by 10%. We still have some work to do!

A couple suggestions to improve the import graph even more.

[BoltonBailey]

This will collide with #21530

Frankly, that PR is much more extensive splitting and should be reviewed and merged first, possibly this PR can just be closed if so.

[kim-em]

I didn't touch take and drop in the PR, so I'm hopeful we can just do both.

[kim-em]

I've merged master now, it will at least need a shake --fix still.

[kim-em]

bors d+

[mathlib-bors]

✌️ BoltonBailey can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.