feat: various small list/array/vector API improvements

[datokrat]

This PR makes several small improvements to the list/array/vector API:

• It fixes typos in Init.Core.
• It adds List.isSome_min_iff and List.isSome_max_iff.
• It adds grind and simp annotations to various previously unannotated lemmas.
• It adds lemmas for characterizing ∃ x ∈ xs, P x using indices as ∃ (i : Nat), ∃ hi, P (xs[i]), and similar universally quantified lemmas: exists_mem_iff_exists_getElem and forall_mem_iff_forall_getElem.
• It adds Vector.toList_zip.
• It adds map_ofFn and ofFn_getElem for lists/arrays/vectors.

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 36bde59 against e56351d are in! @datokrat

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Runner for run build has different system configurations between commits.
• Runner for run other has different system configurations between commits.

Small changes (2✅, 10🟥)

• 🟥 build/module/Init.Data.Array.Count//instructions: +61.3M (+1.8%)
• 🟥 build/module/Init.Data.Array.Lemmas//instructions: +246.4M (+0.3%)
• 🟥 build/module/Init.Data.Array.OfFn//instructions: +189.2M (+7.9%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.List.Count//instructions: +68.1M (+1.8%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.List.Lemmas//instructions: +151.8M (+0.3%)
• 🟥 build/module/Init.Data.List.MinMax//instructions: +66.2M (+1.6%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.List.OfFn//instructions: +179.8M (+7.7%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.Vector.Count//instructions: +71.3M (+2.3%)
• 🟥 build/module/Init.Data.Vector.Lemmas//instructions: +347.7M (+0.6%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.Vector.OfFn//instructions: +117.4M (+1.7%) (reduced significance based on *//lines)
• ✅ build/module/Lake.CLI//instructions: -15.6M (-2.0%)
• ✅ build/module/Lean.Elab.Tactic.Congr//instructions: -18.0M (-1.7%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-12 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-01-15 17:29:26)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-14 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-01-17 00:29:41)

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-12017 build failed against this PR. (2026-01-15 17:42:30) View Log
• 💥 Mathlib branch lean-pr-testing-12017 build failed against this PR. (2026-01-16 13:39:51) View Log
• 💥 Mathlib branch lean-pr-testing-12017 build failed against this PR. (2026-01-16 14:27:22) View Log
• ✅ Mathlib branch lean-pr-testing-12017 has successfully built against this PR. (2026-01-16 15:49:07) View Log
• ✅ Mathlib branch lean-pr-testing-12017 has successfully built against this PR. (2026-01-17 01:37:09) View Log

[datokrat]

I'm not really happy with this approach of grindifying countP_eq_zero, but I couldn't come up with something better. I tend to think that these grind lemmas are useful, but am not 100% sure that adding them is worth it.