perf: parallelize `rw?` tactic

[kim-em]

This PR parallelizes the rw? tactic.

• Use MetaM.parIterWithCancel to try all candidate rewrites in parallel while preserving deterministic result ordering
• When an rfl-closeable result is found (and stopAtRfl is true), or the maximum number of results is reached, remaining tasks are cancelled
• Removes old sequential takeListAux implementation and RewriteResultConfig structure

🤖 Generated with Claude Code

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e1f8c147e72504b88f7275005df32e892e19a08b --onto b0e6db322421ce368999f08870fd747e45242f86. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-26 03:49:49)
• ✅ Mathlib branch lean-pr-testing-11371 has successfully built against this PR. (2025-11-26 06:00:56) View Log
• ✅ Mathlib branch lean-pr-testing-11371 has successfully built against this PR. (2025-12-02 09:34:32) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e1f8c147e72504b88f7275005df32e892e19a08b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-26 03:49:51)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-26 05:01:36)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-02 08:33:57)

[kim-em]

It's not clear this is a win. The overhead of parallelisation could easily exceed the gains. Measurements (perhaps with chunking?) are probably warranted.