feat: upstream slice API improvements from human-eval-lean

[datokrat]

This PR improves the slice API with lemmas for drop/take operations on Subarray and more lemmas about Std.Slice.fold, Std.Slice.foldM and Std.Slice.forIn. It also changes the simp and grind annotations for Slice-related lemmas. Lemmas converting between slices of different shapes are no longer simp/grind-annotated because they often complicated lemmas and hindered automation.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9b7a8eb7c88aa4c93cb59ba07777c1827daec2fa --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-06 15:54:42)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9b7a8eb7c88aa4c93cb59ba07777c1827daec2fa --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force reference manual CI using the force-manual-ci label. (2026-02-06 15:54:44)