perf: map Array.mapFinIdx/mapIdx in place

`Array.mapFinIdxM` (and hence `mapFinIdx`, `mapIdxM`, `mapIdx`) ran only its
push-based reference implementation: it reads each element with `as[i]`, a
borrow that leaves the element shared with the still-live input array. Any
in-place work the mapping function attempts on an element therefore copies it,
so a column-style operation that touches one entry of each row of an
`Array (Array _)` is O(rows * cols) instead of O(rows), and the gap widens
without bound as the rows get wider.

Give `mapFinIdxM` an `@[implemented_by]` unsafe implementation mirroring
`mapMUnsafe`: it nulls each slot (`uset i default`) before invoking `f`, so on a
uniquely-owned input each element arrives exclusive (refcount 1) and may be
mutated in place. The reference body is unchanged, so every lemma about
`mapFinIdxM` still holds; the `@[inline]` is dropped (kept `@[expose]`) because
inlining the reference body at call sites would bypass `@[implemented_by]`, just
as `mapM` is not `@[inline]`.

tests/compile/arrayMapIdxInPlace.lean is a deterministic regression test using
`dbgTraceIfShared`: before this change the `mapFinIdx`/`mapIdx` cases each
printed one "row shared" trace per row; now they print none, matching
`Array.map`.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>