perf: optimize ToJson derive handler

[Kha]

Partially evaluate mkObj call to avoid allocations

[Kha]

!bench

[leanprover-radar]

Benchmark results for f60042a against 0a8abcb are in. There are significant results. @Kha

• 🟥 build//instructions: +2.3G (+0.02%)

Large changes (4✅)

• ✅ vcgen/GetThrowSet/800/kernel//wall-clock: -60ms (-10.12%)
• ✅ vcgen/MatchIota/1000/kernel//wall-clock: -71ms (-16.21%)
• ✅ vcgen/MatchIota/1500/kernel//wall-clock: -169ms (-18.25%)
• ✅ vcgen/MatchIota/500/kernel//wall-clock: -18ms (-12.50%)

Medium changes (2🟥)

• 🟥 size/all/.c//lines: +53.2k (+0.45%)
• 🟥 size/all/.ir//bytes: +2MiB (+0.47%)

Small changes (4✅, 33🟥)

Too many entries to display here. View the full report on radar instead.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-24 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. (2026-06-25 22:04:12)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14186 has successfully built against this PR. (2026-06-25 23:02:10) View Log