fix: re-apply "mark Id.run as [implicit_reducible]"

[kim-em]

This PR re-applies #12757 (reverted in #12801) with the release-ci label to test whether it causes the async extension PANIC seen in the v4.29.0-rc5 tag CI.

🤖 Prepared with Claude Code

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 333ab1c6f0ce11f33551d6a736054cb72812cad9 --onto f3752861c934c277630cc0dc5a812bbcc8b6f3a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-05 08:08:50)

[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 333ab1c6f0ce11f33551d6a736054cb72812cad9 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-05 08:08:52)