feat: beta reduce while elaborating applications

[kmill]

This PR modifies the app elaborator to beta reduce arguments while substituting them into expected types for later arguments. This makes it consistent with inferType and instantiateMVars, which both beta reduce substitutions. In particular, this change ensures that the app elaborator behaves as if it creates metavariables for each parameter and assigns elaborated arguments to the metavariables. Breaking change: tactic proofs may need to be modified to remove unnecessary steps, e.g. dsimp only steps that were previously for beta reductions.

[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 65b34530d3a1b02425090cc4818abd85d361056a --onto 43ef70db63e2c1c1720b84fd153125c96a00c5d2. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-20 21:53:57)
• 💥 Mathlib branch lean-pr-testing-13807 build failed against this PR. (2026-05-21 06:10:49) View Log
• 💥 Mathlib branch lean-pr-testing-13807 build failed against this PR. (2026-05-21 06:57:20) View Log
• 🟡 Mathlib branch lean-pr-testing-13807 build against this PR was cancelled. (2026-05-21 07:28:33) View Log
• ✅ Mathlib branch lean-pr-testing-13807 has successfully built against this PR. (2026-05-21 07:45:59) 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 65b34530d3a1b02425090cc4818abd85d361056a --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-20 21:53:58)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-20 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-05-21 06:00:34)

[kmill]

!bench

[leanprover-radar]

Benchmark results for 194b71e against 65b3453 are in. No significant results found. @kmill

• ✅ build//instructions: -786.4M (-0.01%)

Small changes (4✅, 2🟥)

• ✅ build/module/Init.Data.Iterators.Consumers.Access//instructions: -472.1M (-18.31%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Iterators.Lemmas.Consumers.Collect//instructions: -236.9M (-10.76%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect//instructions: -69.3M (-2.36%)
• 🟥 build/module/Init.WFExtrinsicFix//instructions: +129.6M (+2.25%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Zip//instructions: -121.7M (-1.35%) (reduced significance based on absolute threshold)
• 🟥 mvcgen/sym/AddSubCancel/100/kernel//wall-clock: +3ms (+15.79%)

[kmill]

!bench

[leanprover-radar]

Benchmark results for 748dd85 against 727b4aa are in. No significant results found. @kmill

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

Small changes (6✅, 1🟥)

• ✅ build/module/Init.Data.Iterators.Consumers.Access//instructions: -472.1M (-18.30%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Iterators.Lemmas.Consumers.Collect//instructions: -239.0M (-10.84%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect//instructions: -75.5M (-2.56%)
• ✅ build/module/Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop//instructions: -50.1M (-0.41%)
• ✅ build/module/Init.Data.Vector.Attach//instructions: -45.4M (-0.66%)
• 🟥 build/module/Init.WFExtrinsicFix//instructions: +126.0M (+2.19%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Zip//instructions: -138.1M (-1.52%) (reduced significance based on absolute threshold)