perf: make isRfl lazy

[Kha]

No description provided.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-7719 build failed against this PR. (2025-03-29 13:52:59) View Log
• 💥 Mathlib branch lean-pr-testing-7719 build failed against this PR. (2025-03-30 11:26:02) View Log
• ✅ Mathlib branch lean-pr-testing-7719 has successfully built against this PR. (2025-04-02 10:36:24) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dedfbaf521084ae78d0a826de8b3bab8fd5a3ebd --onto 911ea07a73733650eefa5240652404856bdcceb7. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-02 13:43:14)

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit ece4c21.Found no runs to compare against.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit ece4c21.
There were significant changes against commit dedfbaf:

  Benchmark                              Metric                    Change
  ==================================================================================
- Init.Data.BitVec.Lemmas                branch-misses               5.7%   (10.2 σ)
- Init.Data.BitVec.Lemmas                task-clock                 18.3%   (23.5 σ)
+ Init.Data.BitVec.Lemmas                wall-clock                -27.3%  (-69.1 σ)
- Init.Data.BitVec.Lemmas re-elab        branch-misses             101.3%  (564.4 σ)
- Init.Data.BitVec.Lemmas re-elab        branches                   21.7%  (528.0 σ)
- Init.Data.BitVec.Lemmas re-elab        instructions               24.3%  (451.2 σ)
- Init.Data.BitVec.Lemmas re-elab        maxrss                     53.4%   (16.4 σ)
- Init.Data.BitVec.Lemmas re-elab        task-clock                120.0%  (195.6 σ)
- Init.Data.BitVec.Lemmas re-elab        wall-clock                 47.3%   (61.7 σ)
+ Init.Data.List.Sublist re-elab -j4     wall-clock                 -3.6%  (-13.9 σ)
- Std.Data.DHashMap.Internal.RawLemmas   task-clock                  4.2%  (139.8 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   wall-clock                -19.9%  (-83.6 σ)
+ bv_decide_large_aig.lean               task-clock                 -4.3%  (-22.7 σ)
+ bv_decide_large_aig.lean               wall-clock                 -4.4%  (-21.7 σ)
- bv_decide_mul                          maxrss                      1.4%  (189.3 σ)
+ lake build no-op                       wall-clock                 -9.3%  (-22.3 σ)
+ reduceMatch                            task-clock                 -1.1%  (-12.9 σ)
+ stdlib                                 attribute application      -3.4%  (-11.1 σ)
- stdlib                                 blocked (unaccounted)      10.2% (1207.6 σ)
- stdlib                                 process pre-definitions     3.7%   (18.8 σ)
- stdlib                                 tactic execution            7.8%   (12.1 σ)
- stdlib                                 task-clock                  1.1%   (22.8 σ)
+ stdlib                                 wall-clock                 -6.1%  (-22.1 σ)
+ unionfind                              task-clock                -20.9%  (-30.6 σ)
+ unionfind                              wall-clock                -20.9%  (-30.6 σ)