fix: avoid exposing Fin.foldl implementation

[kernelpanic888]

This PR restores the performance boundary inside Fin.foldl, preventing simp only from descending through the recursive loop and exhausting the default heartbeat budget.

The outer Fin.foldl remains @[expose] so existing kernel reduction continues to work; only the inner loop is no longer semireducible.

Closes #14540.

The regression test simplifies the issue expression in a hypothesis at the default heartbeat limit. Follow-up commit 12c7e25f6c also preserves the existing finFoldKernelReduce behavior exposed by full CI.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-25 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-07-25 20:06:11)

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-14554 has successfully built against this PR. (2026-07-25 20:11:22) View Log
• 🟡 Reference manual branch lean-pr-testing-14554 build against this PR didn't complete normally. (2026-07-25 20:12:50) View Log
• ✅ Reference manual branch lean-pr-testing-14554 has successfully built against this PR. (2026-07-30 21:03:31) View Log
• 🟡 Reference manual branch lean-pr-testing-14554 build against this PR didn't complete normally. (2026-07-30 21:05:01) View Log