fix: add checkSystem calls to long-running elaboration paths

This PR adds `checkSystem` calls to several code paths that can run for
extended periods without checking for cancellation, heartbeat limits, or
stack overflow. This improves responsiveness of the cancellation mechanism
in the language server.

Affected paths:
- `simp` rewrite candidate loops (`Rewrite.lean`)
- `simpAppUsingCongr` argument traversal (`Types.lean`)
- `synthesizeSyntheticMVarsStep` mvar loop (`SyntheticMVars.lean`)
- `abstractNestedProofs` visitor (`AbstractNestedProofs.lean`)
- `transform`/`transformWithCache` visitors (`Transform.lean`)
- LCNF compiler pass runner loop (`Main.lean`)
- LCNF checker recursive traversal (`Check.lean`)
- LCNF simplifier recursive traversal (`Simp/Main.lean`)
- `whnfCore` recursive reduction loop (`WHNF.lean`)

With these changes, at a 50ms monitoring threshold across the full test suite,
the only remaining Lean-side elaborator gaps are:
- bv_decide pure computation wrapped in `IO.lazyPure` (architectural)
- Single deep `whnf` reductions from the `constructorNameAsVariable` linter (~100-180ms)

Remaining C++ gaps (type checker, interpreter module init) are tracked separately.

Found using `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring from #13218.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>