fix: find realizations from other env branches

[Kha]

No description provided.

[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 a8a5c6cff1208d80517c05a1d4ac38dcadfb4030 --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-07 21:10:03)
  Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-03-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2025-03-08 11:26:12)
• ✅ Mathlib branch lean-pr-testing-7385 has successfully built against this PR. (2025-03-08 12:14:47) View Log
• ✅ Mathlib branch lean-pr-testing-7385 has successfully built against this PR. (2025-03-08 17:54:33) View Log
• 💥 Mathlib branch lean-pr-testing-7385 build failed against this PR. (2025-03-08 19:42:55) View Log
• ✅ Mathlib branch lean-pr-testing-7385 has successfully built against this PR. (2025-03-10 09:35:54) View Log
• ✅ Mathlib branch lean-pr-testing-7385 has successfully built against this PR. (2025-03-10 11:48:29) View Log
  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 22b6b49a432bdfdb8a916f3f9b41a2e7b61594c1 --onto 7bfa8f6296ebfebc497d5b30d34f494bcc9782a2. (2025-03-10 16:17:23)
• ✅ Mathlib branch lean-pr-testing-7385 has successfully built against this PR. (2025-03-10 17:05:35) View Log

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 4da709f.
There were significant changes against commit 565c6f3:

  Benchmark                      Metric               Change
  =====================================================================
- Init.Data.List.Sublist async   branches               1.1%   (96.7 σ)
- Init.Prelude async             branches              10.9% (1757.0 σ)
- Init.Prelude async             instructions           8.8% (1295.7 σ)
+ Init.Prelude async             maxrss                -4.3%  (-35.7 σ)
- identifier auto-completion     branches               5.9%  (783.4 σ)
- identifier auto-completion     instructions           5.1%  (602.6 σ)
- stdlib                         blocked              161.9%  (588.7 σ)
- stdlib                         dsimp                  5.5%  (108.7 σ)
+ stdlib                         share common exprs    -4.8%  (-12.5 σ)
+ stdlib                         type checking         -2.2%  (-19.5 σ)
- stdlib                         wall-clock             9.4%   (13.9 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 43f0b0b.
There were significant changes against commit 565c6f3:

  Benchmark                      Metric                  Change
  ========================================================================
+ Init.Data.List.Sublist async   branches                 -2.1% (-202.2 σ)
+ Init.Data.List.Sublist async   instructions             -1.7% (-153.8 σ)
- Init.Data.List.Sublist async   wall-clock               12.7%   (11.5 σ)
- Init.Prelude async             wall-clock               15.1%   (21.1 σ)
+ reduceMatch                    instructions             -1.3%  (-52.5 σ)
- stdlib                         attribute application    12.4%   (19.3 σ)
- stdlib                         blocked                 152.4%   (87.7 σ)
+ stdlib                         dsimp                    -4.0%  (-14.4 σ)
- stdlib                         instantiate metavars      5.1%   (15.5 σ)
+ stdlib                         share common exprs       -2.9%  (-10.6 σ)
+ stdlib                         tactic execution         -3.4%  (-22.6 σ)
+ stdlib                         task-clock               -2.5%  (-12.3 σ)
+ stdlib                         type checking            -2.4%  (-17.3 σ)
- stdlib                         wall-clock               10.7%   (23.4 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 097a8f0.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1fddb60.
There were significant changes against commit 565c6f3:

  Benchmark                      Metric               Change
  ======================================================================
+ Init.Data.List.Sublist async   branches              -2.3%  (-362.4 σ)
+ Init.Data.List.Sublist async   instructions          -1.9%  (-291.8 σ)
+ Init.Prelude async             branches              -7.2%  (-226.2 σ)
+ Init.Prelude async             instructions          -5.8%  (-157.2 σ)
+ identifier auto-completion     branches             -16.0% (-1050.4 σ)
+ identifier auto-completion     instructions         -13.5%  (-799.2 σ)
+ identifier auto-completion     task-clock           -11.5%   (-10.3 σ)
+ reduceMatch                    instructions          -1.4%   (-57.4 σ)
+ stdlib                         dsimp                 -7.2%   (-50.5 σ)
+ stdlib                         instructions          -1.5%  (-297.9 σ)
+ stdlib                         share common exprs    -3.6%   (-20.2 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit f3b921d.
There were significant changes against commit 565c6f3:

  Benchmark                      Metric         Change
  ===============================================================
+ Init.Data.List.Sublist async   branches        -2.3% (-125.7 σ)
+ Init.Data.List.Sublist async   instructions    -1.9%  (-91.2 σ)
+ Init.Prelude async             branches        -7.3% (-229.6 σ)
+ Init.Prelude async             instructions    -5.9% (-156.4 σ)
+ identifier auto-completion     branches       -16.2% (-872.1 σ)
+ identifier auto-completion     instructions   -13.6% (-714.1 σ)
+ reduceMatch                    instructions    -1.4%  (-39.4 σ)
+ stdlib                         instructions    -1.5% (-142.5 σ)
+ stdlib                         task-clock      -1.2%  (-25.2 σ)