[Merged by Bors] - perf(Translate): don't actually beta reduce the proof

[JovanGerb]

This PR does the fix of #37756 without actually beta reducing any terms. It turns out that sometimes beta reducing can be very expensive. (I knew that this is true in theory, but I'm surprised that it's also true in practice)

---

[github-actions]

PR summary cb3293da5d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 3e3c9a1 against cb3293d are in. Significant changes detected! @JovanGerb

• 🟥 main exited with code 1

No significant changes detected.

[JovanGerb]

Let's try again

!bench

[leanprover-radar]

Benchmark results for 96c28d5 against cb3293d are in. Significant changes detected! @JovanGerb

• ✅ build//instructions: -627.6G (-0.36%)

Large changes (4✅, 14🟥)

• ✅ build//wall-clock: -1m 15s (-11.45%)
• ✅ build/lakeprof/longest build path//wall-clock: -1m 13s (-11.44%)
• ✅ build/lakeprof/longest rebuild path//wall-clock: -1m 13s (-11.87%)
• ✅ build/module/Mathlib.Topology.Algebra.InfiniteSum.Constructions//instructions: -554.1G (-90.14%)
• 🟥 build/profile/aesop//wall-clock: +20s (+8.83%)
• 🟥 build/profile/attribute application//wall-clock: +10s (+11.25%)
• 🟥 build/profile/congr simp thm//wall-clock: +11s (+16.21%)
• 🟥 build/profile/elaboration//wall-clock: +4m 54s (+12.58%)
• 🟥 build/profile/import//wall-clock: +9m 7s (+8.86%)
• 🟥 build/profile/interpretation//wall-clock: +10m 26s (+7.03%)
• 🟥 build/profile/linting//wall-clock: +24s (+9.59%)
• 🟥 build/profile/parsing//wall-clock: +11s (+8.66%)
• 🟥 build/profile/process pre-definitions//wall-clock: +37s (+19.55%)
• 🟥 build/profile/share common exprs//wall-clock: +7s (+11.82%)
• 🟥 build/profile/simp//wall-clock: +3m 43s (+10.25%)
• 🟥 build/profile/tactic execution//wall-clock: +4m 15s (+11.35%)
• 🟥 build/profile/type checking//wall-clock: +2m 13s (+7.87%)
• 🟥 build/profile/typeclass inference//wall-clock: +15m 13s (+12.61%)

Medium changes (10🟥)

• 🟥 build/profile/.olean serialization//wall-clock: +57s (+6.83%)
• 🟥 build/profile/C code generation//wall-clock: +507ms (+4.63%)
• 🟥 build/profile/blocked (unaccounted)//wall-clock: +5m 38s (+9.98%)
• 🟥 build/profile/dsimp//wall-clock: +13s (+12.40%)
• 🟥 build/profile/fix level params//wall-clock: +2s (+9.69%)
• 🟥 build/profile/grind//wall-clock: +10s (+9.02%)
• 🟥 build/profile/initialization//wall-clock: +16s (+6.89%)
• 🟥 build/profile/let-to-have transformation//wall-clock: +6s (+13.22%)
• 🟥 build/profile/norm_num//wall-clock: +3s (+28.00%)
• 🟥 build/profile/sym typeclass inference//wall-clock: +30s (+12.33%)

Small changes (2✅, 10🟥)

• ✅ build//instructions: -627.6G (-0.36%)
• 🟥 build/module/Mathlib.Data.Fin.Tuple.BubbleSortInduction//instructions: +271.1M (+4.96%)
• ✅ build/module/Mathlib.Data.Rat.Encodable//instructions: -245.7M (-5.74%)
• 🟥 build/module/Mathlib.Util.PrintSorries//instructions: +137.7M (+3.28%)
• 🟥 build/profile/compilation (LCNF base)//wall-clock: +7s (+4.13%)
• 🟥 build/profile/compilation (LCNF impure)//wall-clock: +1s (+5.36%)
• 🟥 build/profile/compilation (LCNF mono)//wall-clock: +4s (+5.29%)
• 🟥 build/profile/grind mark subsingleton//wall-clock: +1s (+6.86%)
• 🟥 build/profile/grind simp//wall-clock: +4s (+6.96%)
• 🟥 build/profile/instantiate metavars//wall-clock: +2s (+11.65%)
• 🟥 build/profile/ring//wall-clock: +5s (+18.30%)
• 🟥 build/profile/sym canon//wall-clock: +2s (+10.82%)

and 1 hidden

[bryangingechen]

Thanks!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job
• ci (staging) / Lint style