feat: add chunking support to par and par' in Lean.Elab.Parallel

This PR adds optional chunking support to the `par` and `par'` functions in
`Lean.Elab.Parallel` for CoreM, MetaM, TermElabM, and TacticM. This reduces
task creation overhead when there are many small jobs by grouping them into
chunks that run sequentially within each parallel task.

New optional parameters:
- `maxTasks : Nat := 0` - Maximum number of parallel tasks (0 = no limit)
- `minChunkSize : Nat := 1` - Minimum jobs per chunk

Example: With 1000 jobs and `maxTasks := 128, minChunkSize := 8`:
- Chunk size = max(8, ceil(1000/128)) = 8
- Creates ~125 parallel tasks instead of 1000

Default behavior (maxTasks = 0) is unchanged - one task per job.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <[email protected]>

Author: kim-em