feat: add simp lemma writing Vector.tail in terms of Vector.extract

[kim-em]

This PR adds a @[simp] lemma, and comments explaining that there is intentionally no verification API for Vector.take, Vector.drop, or Vector.tail, which should all be rewritten in terms of Vector.extract.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5e40f4af52c50ff670c2b09b87930b42ff30a6ba --onto 4eccb5b4792c270ad10ac059b9672a8845961079. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-22 23:31:59)