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)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-08 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-02-09 14:14:42)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12352 has successfully built against this PR. (2026-02-09 15:14:48) View Log

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 8e874ca against 39c26fc are in! @datokrat

• 🟥 build//instructions: +4.8G (+0.04%)

Medium changes (1🟥)

• 🟥 build/module/Init.Data.Slice.Lemmas//bytes .olean: +16kiB (+22.96%)

Small changes (6✅, 12🟥)

• 🟥 build/module/Init.Data.Slice.Array.Lemmas//bytes .ilean: +15kiB (+16.56%)
• 🟥 build/module/Init.Data.Slice.Array.Lemmas//bytes .olean: +40kiB (+19.09%)
• 🟥 build/module/Init.Data.Slice.Array.Lemmas//bytes .olean.private: +311kiB (+35.13%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.Slice.Array.Lemmas//bytes .olean.server: +5kiB (+14.78%)
• 🟥 build/module/Init.Data.Slice.Array.Lemmas//instructions: +2.8G (+23.00%) (reduced significance based on *//lines)
• ✅ build/module/Init.Data.Slice.Lemmas//bytes .ilean: -3kiB (-22.54%) (reduced significance based on *//lines)
• ✅ build/module/Init.Data.Slice.Lemmas//bytes .olean.server: -1kiB (-27.20%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.Slice.Lemmas//instructions: +69.2M (+7.40%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Slice.List.Lemmas//instructions: +485.4M (+7.67%) (reduced significance based on *//lines)
• ✅ build/module/Lean.Elab.PreDefinition.MkInhabitant//instructions: -18.0M (-0.54%)
• 🟥 build/module/Lean.Elab.Tactic.Grind.LintExceptions//instructions: +23.6M (+1.79%)
• ✅ build/module/Lean.Meta.HasNotBit//instructions: -15.3M (-1.42%)
• ✅ build/module/Lean.Server.Completion//instructions: -21.0M (-1.16%)
• ✅ build/module/Lean.Server.Snapshots//instructions: -20.8M (-1.97%)
• 🟥 build/module/Std.Data.Iterators.Lemmas.Producers.Slice//bytes .ilean: +4kiB (+31.38%) (reduced significance based on *//lines)
• 🟥 build/module/Std.Data.Iterators.Lemmas.Producers.Slice//bytes .olean.private: +10kiB (+56.35%) (reduced significance based on *//lines)
• 🟥 build/module/Std.Data.Iterators.Lemmas.Producers.Slice//bytes .olean.server: +696B (+16.32%)
• 🟥 build/module/Std.Data.Iterators.Lemmas.Producers.Slice//instructions: +155.3M (+22.17%) (reduced significance based on *//lines)