[Merged by Bors] - fix(Translate): beta reduce proof before translation

[JovanGerb]

Some tactics may generate proofs terms containing beta expanded terms. Such terms are annoying for the to_additive/to_dual heuristic, because then the heuristic sees a variable rather than the term that it is actually supposed to look at. The fix is to beta reduce such proof terms.

---

[github-actions]

PR summary fcdb939818

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ le_of_lt_and_le_of_lt

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).

[bryangingechen]

Thanks!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

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

[JovanGerb]

It seems like this PR may have caused some horrible performance drop??

!bench

[leanprover-radar]

Benchmark results for 6b38c8e against fcdb939 are in. Significant changes detected! @JovanGerb

• 🟥 build//instructions: +613.1G (+0.35%)

Large changes (15✅, 4🟥)

• 🟥 build//wall-clock: +1m 15s (+12.88%)
• 🟥 build/lakeprof/longest build path//wall-clock: +1m 18s (+13.69%)
• 🟥 build/lakeprof/longest rebuild path//wall-clock: +1m 16s (+14.05%)
• 🟥 build/module/Mathlib.Topology.Algebra.InfiniteSum.Constructions//instructions: +553.5G (+910.65%)
• ✅ build/profile/aesop//wall-clock: -20s (-8.09%)
• ✅ build/profile/attribute application//wall-clock: -9s (-9.31%)
• ✅ build/profile/congr simp thm//wall-clock: -11s (-14.01%)
• ✅ build/profile/elaboration//wall-clock: -4m 56s (-11.21%)
• ✅ build/profile/import//wall-clock: -8m 51s (-7.91%)
• ✅ build/profile/initialization//wall-clock: -18s (-7.28%)
• ✅ build/profile/interpretation//wall-clock: -10m 57s (-6.87%)
• ✅ build/profile/linting//wall-clock: -24s (-8.52%)
• ✅ build/profile/parsing//wall-clock: -11s (-7.87%)
• ✅ build/profile/process pre-definitions//wall-clock: -36s (-15.96%)
• ✅ build/profile/share common exprs//wall-clock: -7s (-10.47%)
• ✅ build/profile/simp//wall-clock: -3m 45s (-9.38%)
• ✅ build/profile/tactic execution//wall-clock: -4m 22s (-10.45%)
• ✅ build/profile/type checking//wall-clock: -2m 2s (-6.72%)
• ✅ build/profile/typeclass inference//wall-clock: -15m 22s (-11.29%)

Medium changes (10✅)

• ✅ build/profile/.olean serialization//wall-clock: -1m 2s (-6.93%)
• ✅ build/profile/C code generation//wall-clock: -409ms (-3.60%)
• ✅ build/profile/blocked (unaccounted)//wall-clock: -5m 42s (-9.16%)
• ✅ build/profile/dsimp//wall-clock: -14s (-11.86%)
• ✅ build/profile/fix level params//wall-clock: -2s (-8.56%)
• ✅ build/profile/grind//wall-clock: -9s (-7.99%)
• ✅ build/profile/let-to-have transformation//wall-clock: -5s (-10.55%)
• ✅ build/profile/norm_num//wall-clock: -4s (-23.96%)
• ✅ build/profile/ring//wall-clock: -6s (-17.46%)
• ✅ build/profile/sym typeclass inference//wall-clock: -29s (-10.77%)

Small changes (7✅, 2🟥)

• 🟥 build//instructions: +613.1G (+0.35%)
• 🟥 build/module/Mathlib.Tactic.Explode.Pretty//instructions: +384.4M (+14.31%)
• ✅ build/profile/compilation (LCNF base)//wall-clock: -7s (-4.05%)
• ✅ build/profile/compilation (LCNF impure)//wall-clock: -1s (-3.66%)
• ✅ build/profile/compilation (LCNF mono)//wall-clock: -4s (-4.98%)
• ✅ build/profile/grind mark subsingleton//wall-clock: -888ms (-5.50%)
• ✅ build/profile/grind simp//wall-clock: -4s (-6.91%)
• ✅ build/profile/instantiate metavars//wall-clock: -2s (-10.92%)
• ✅ build/profile/sym canon//wall-clock: -2s (-9.67%)

and 1 hidden

[kbuzzard]

Oh wow this really does seem to be true!

On commit fcdb9398187d650167215e8ce644dac16f2883fd the lemma HasProd.sum in Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean profiles at 6228610 heartbeats whereas on commit 5d32f3eac7f8cc9f39e46ab0d7e0c1722d6d2a4e (this PR) it is an astronomical 380612519. This is using

set_option trace.profiler.useHeartbeats true in
set_option trace.profiler true in

The problem is to_additive taking a long time: see https://gist.github.com/kbuzzard/f69a089805d39123a7ad5175f49cc1fb and compare with https://gist.github.com/kbuzzard/766fa711cefb620e10048c9587d89318

[bryangingechen]

Wow, I should have remembered to run !bench. @JovanGerb if you don't see a quick fix (i.e. can be merged within a day or two), shall we revert this?

[JovanGerb]

I've made an attempt at fixing this in #37776