feat: standalone List.extract lemmas, don't normalize extract into drop/take

[datokrat]

This PR contains a significant breaking change regarding the simp behavior of List.extract and Array.extract. Previously, simp rewrote both automatically (and suboptimally) into a combination of take and drop. Now, extract keeps being extract. The change introduces lemmas for List.extract that are needed now that we don't normalize to take/drop anymore.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-01 16:37:19)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-01 16:37:21)