perf: improve proof-over-applied cases in ToLCNF

[Rob23oba]

This PR changes the handling of proof-over-applied cases expressions in ToLCNF to avoid generating function declarations that are called immediately. This is a less invasive version of #12284 (which has since been reverted) that only affects proof overapplications, not all overapplications. However, this is also the only case we really need for #8309 (and other occasions like match h : _).

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-05 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-03-05 18:02:27)

[Rob23oba]

!bench

[leanprover-radar]

Benchmark results for b29fa21 against 333ab1c are in! @Rob23oba

• ✅ build//instructions: -1.0G (-0.01%)

Small changes (7✅, 8🟥)

• ✅ build/module/Lean.Compiler.LCNF.LambdaLifting//instructions: -32.0M (-0.77%)
• 🟥 build/module/Lean.Compiler.LCNF.ToLCNF//instructions: +1.1G (+5.78%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Elab.Do.InferControlInfo//instructions: +152.1M (+1.00%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.Reify//instructions: -23.2M (-0.34%)
• 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Simproc//instructions: +337.9M (+0.94%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Elab.Tactic.Do.ProofMode.Specialize//instructions: -24.4M (-0.45%)
• 🟥 build/module/Lean.Elab.Tactic.Do.VCGen//instructions: +95.1M (+0.29%)
• 🟥 build/module/Lean.Meta.CasesInfo//instructions: +25.8M (+1.57%)
• ✅ build/module/Lean.Meta.LitValues//instructions: -36.7M (-0.88%)
• 🟥 build/module/Lean.Meta.Tactic.Grind.Canon//instructions: +62.7M (+0.54%)
• 🟥 build/module/Lean.Meta.Tactic.Grind.MarkNestedSubsingletons//instructions: +29.0M (+0.70%)
• 🟥 build/module/Std.Do.SPred.Notation//instructions: +72.7M (+0.36%)
• ✅ build/module/Std.Internal.Http.Data.Status//instructions: -55.0M (-0.79%)
• ✅ elab/big_beq//instructions: -54.3M (-0.54%)
• ✅ elab/big_beq_rec//instructions: -65.1M (-0.34%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12814 has successfully built against this PR. (2026-03-05 19:09:04) View Log