perf: in CaseValues, subst only once

[nomeata]

This PR avoids running substCore twice in caseValues.

[nomeata]

!radar

[leanprover-radar]

Benchmark results for 3ee6542 against e548fa4 are in! @nomeata

Major changes (2)

• ✅ big_match_nat//instructions: -40.3G (-56.9%)
• ✅ big_match_nat_split//instructions: -17.5G (-51.6%)

[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 e548fa414cb74db21a31afe6c26cb0c51310f1db --onto 0173444d24df9253d7947cfe82519e4a6caffd3a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 11:27:06)

[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 e548fa414cb74db21a31afe6c26cb0c51310f1db --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-04 11:27:08)

[nomeata]

Very nice radar results. I wonder if they add to those of #11508. But probably they are a subset of those.

[nomeata]

!radar

[leanprover-radar]

Benchmark results for 98a06ec against 0173444 are in! @nomeata

[nomeata]

Sorry for the accidential merge into nightly-with-mathlib. I blame Github for refusing to run CI just because there is a conflict with master. Second try at #11510