fix: expose Array.ofFn for kernel reduction

[kim-em]

This PR lets Array.ofFn and the delegating Vector.ofFn reduce in the kernel across module boundaries.

Expose Array.ofFn; exposure covers the where helper that performs the construction. Direct rfl regressions verify reduction of the array size, array value, and vector value without depending on either DecidableEq fix.

Split from the original #14270 alongside the independent Vector DecidableEq fix in #14988.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-09-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-01 14:11:36)

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-14989 has successfully built against this PR. (2026-09-01 14:17:53) View Log
• 🟡 Reference manual branch lean-pr-testing-14989 build against this PR didn't complete normally. (2026-09-01 14:18:30) View Log