feat: improve performance of instantiateBetaRevRange

[kmill]

This PR improves Expr.instantiateBetaRevRange to be more efficient in the common case where lambda functions are not being instantiated, and it increases expression sharing in applications.

The motivation is that we would like to use this function more pervasively in elaboration, so that users do not need to write dsimp only as frequently in applications that involve higher-order functions, plus inferType uses it so there is a UX inconsistency when the elaborator is not using it.

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-13758 has successfully built against this PR. (2026-05-16 17:22:55) View Log
• 🟡 Reference manual branch lean-pr-testing-13758 build against this PR didn't complete normally. (2026-05-16 17:23:58) View Log

[kmill]

!bench

[leanprover-radar]

Benchmark results for 15fbdf0 against 803553a are in. There are significant results. @kmill

• ✅ build//instructions: -35.4G (-0.31%)

Medium changes (5✅)

• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: -1.2G (-1.83%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -1.5G (-1.47%)
• ✅ elab/big_match//instructions: -72.0M (-0.66%)
• ✅ elab/omega_stress//instructions: -67.7M (-1.70%)
• ✅ elab/simp_bubblesort_256//instructions: -205.8M (-1.93%)

Small changes (188✅, 3🟥)

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

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13758 has successfully built against this PR. (2026-05-16 18:13:47) View Log