perf: deduplicate core computation inside mkCongrSimpForConst?

[Kha]

No description provided.

[Kha]

!bench

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5778a3c0f2dbe17fdac88902478362d66c43fd61 --onto 18a82c04fc59d3dba392308e09d65ee431240d89. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-11 15:21:52)
  Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-07-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-07-15 09:40:23)
  Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9328271dd0e3710fcc7224db4eddaa79d2b9c8fc --onto cdab726e3d289b80860ae9f5a7de21d990c8b95f. (2025-07-23 16:33:37)

[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 5778a3c0f2dbe17fdac88902478362d66c43fd61 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-11 15:21:53)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-15 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. (2025-07-15 09:40:24)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9328271dd0e3710fcc7224db4eddaa79d2b9c8fc --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-23 16:33:38)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-23 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. (2025-07-24 12:08:38)

[leanprover-bot]

Here are the benchmark results for commit 86fc2aa.
There were significant changes against commit 5778a3c:

  Benchmark                   Metric                  Change
  =====================================================================
- bv_decide_inequality.lean   maxrss                    1.9% (1429.6 σ)
- bv_decide_mod               task-clock                6.9%   (71.8 σ)
- bv_decide_mod               wall-clock                6.8%  (120.9 σ)
+ stdlib                      attribute application    -1.3%  (-36.9 σ)
- treemap.lean                iterate                   4.3%

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit ed5380a.
There were significant changes against commit aac501a:

  Benchmark                   Metric       Change
  ==========================================================
+ bv_decide_inequality.lean   maxrss        -1.5%  (-33.2 σ)
- bv_decide_mod               task-clock     3.0%   (20.3 σ)
- bv_decide_mod               wall-clock     2.9%   (22.1 σ)
- hashmap.lean                iterate        3.5%
- hashmap.lean                task-clock     6.4%   (47.4 σ)
- hashmap.lean                wall-clock     6.4%   (51.7 σ)
- stdlib                      grind          1.7% (1579.0 σ)

[leanprover-community-bot]

• 💥 Mathlib branch lean-pr-testing-9300 build failed against this PR. (2025-07-15 09:56:30) View Log

[leanprover-community-bot]

• 💥 Mathlib branch lean-pr-testing-9300 build failed against this PR. (2025-07-23 16:39:29) View Log

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9c4713c.
There were significant changes against commit 4cbfa48:

  Benchmark                  Metric          Change
  ============================================================
- bv_decide_mod              task-clock        2.4%   (29.9 σ)
- bv_decide_mod              wall-clock        2.3% (1330.5 σ)
- channel.lean               bounded0_spsc    18.3%   (54.3 σ)
+ channel.lean               unbounded_seq    -1.7%
- liasolver                  task-clock        2.8%   (28.3 σ)
- liasolver                  wall-clock        2.8%   (27.2 σ)
+ parser                     task-clock       -7.4%  (-34.8 σ)
+ parser                     wall-clock       -7.4%  (-34.4 σ)
+ stdlib                     grind ring       -3.8%  (-29.2 σ)
- tests/bench/ interpreted   wall-clock        1.9%   (42.0 σ)

[leanprover-community-bot]

• 💥 Mathlib branch lean-pr-testing-9300 build failed against this PR. (2025-07-24 12:51:38) View Log