leanprover-bot

Reference manual CI status: - ✅ Reference manual branch [lean-pr-testing-11435](https://github.com/leanprover-community/mathlib4-nightly-testing/compare/nightly-testing...lean-pr-testing-11435) has successfully built against this PR. (2025-12-07 20:16:40) [View Log](https://github.com/leanprover/reference-manual/actions/runs/20009682681) - 🟡 Reference manual branch [lean-pr-testing-11435](https://github.com/leanprover-community/mathlib4-nightly-testing/compare/nightly-testing...lean-pr-testing-11435) build against this PR...

Reference manual CI status: - ❗ Reference manual CI will not be attempted unless your PR branches off the `nightly-with-manual` branch. Try `git rebase 2ca3bc28590c5c33f755d3bd18252f25ea266266 --onto d3dda9f6d4428a906c096067ecb75e432afc4615`. You can force...

Here are the [benchmark results](https://speed.lean-lang.org/lean4/run-detail/fb5df729-d5e8-485f-94bb-08687a6d46bf) for commit 50c6490075a65e9411bd1cc60275b6def6e438b6. There were [significant changes](https://speed.lean-lang.org/lean4/compare/0f7fbf1a-62b4-4abd-8d14-98814e8fa99d/to/fb5df729-d5e8-485f-94bb-08687a6d46bf) against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577: ```diff Benchmark Metric Change ===================================================== + big_beq_rec branches -2.8% (-261.7 σ) + big_beq_rec instructions -3.0%...

Here are the [benchmark results](https://speed.lean-lang.org/lean4/run-detail/26939fd3-3043-4c9b-b976-ddddde4d8840) for commit b0692312c651883e340f0138a143548f9ea74968. There were [significant changes](https://speed.lean-lang.org/lean4/compare/0f7fbf1a-62b4-4abd-8d14-98814e8fa99d/to/26939fd3-3043-4c9b-b976-ddddde4d8840) against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577: ```diff Benchmark Metric Change ======================================================================== + Init.Data.BitVec.Lemmas branch-misses -2.2% (-33.8 σ) + big_beq_rec branch-misses -3.9%...

Here are the [benchmark results](https://speed.lean-lang.org/lean4/run-detail/e2fbf165-23cb-498b-80c7-5d7d13efd19e) for commit 7fa3a2a8bbef3e07ad27ac96ebcb1127a9d634d5. There were [significant changes](https://speed.lean-lang.org/lean4/compare/0f7fbf1a-62b4-4abd-8d14-98814e8fa99d/to/e2fbf165-23cb-498b-80c7-5d7d13efd19e) against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577: ```diff Benchmark Metric Change ===================================================================== + big_beq_rec branches -2.8% (-117.3 σ) + big_beq_rec instructions -3.0%...

Here are the [benchmark results](https://speed.lean-lang.org/lean4/run-detail/8a75e319-afed-493f-8b7f-0b0b79fd8189) for commit 358c2cfe06b6a0cade339b34c9e15c56678c6813. There were [significant changes](https://speed.lean-lang.org/lean4/compare/0f7fbf1a-62b4-4abd-8d14-98814e8fa99d/to/8a75e319-afed-493f-8b7f-0b0b79fd8189) against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577: ```diff Benchmark Metric Change ===================================================== + big_beq_rec branches -2.8% (-113.9 σ) + big_beq_rec instructions -3.0%...

Here are the [benchmark results](https://speed.lean-lang.org/lean4/run-detail/bb3149bf-1a0e-48bd-9076-1aef5319638c) for commit 6aa113c830a04e5fb515e1c950a7220df4e52f05. There were [significant changes](https://speed.lean-lang.org/lean4/compare/0f7fbf1a-62b4-4abd-8d14-98814e8fa99d/to/bb3149bf-1a0e-48bd-9076-1aef5319638c) against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577: ```diff Benchmark Metric Change ==================================================================== + Init.Data.BitVec.Lemmas branch-misses -2.1% (-85.5 σ) + big_beq_rec branches -2.8%...

Here are the [benchmark results](https://speed.lean-lang.org/lean4/run-detail/c323dbfa-7741-493e-bd5c-9b598a1a7837) for commit 94d2a9ab0b4c43a2c0c5bea65bcc4f15034c277c. The entire run failed. Found no significant differences.

Here are the [benchmark results](https://speed.lean-lang.org/lean4/run-detail/89a6bda0-3f75-4b26-a9b8-4bc1bd3c3d6b) for commit c9a2413da89fb487f34205170b4777d898d729a4. There were [significant changes](https://speed.lean-lang.org/lean4/compare/0f7fbf1a-62b4-4abd-8d14-98814e8fa99d/to/89a6bda0-3f75-4b26-a9b8-4bc1bd3c3d6b) against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577: ```diff Benchmark Metric Change ====================================================== + big_beq_rec branches -2.8% (-156.8 σ) + big_beq_rec instructions -3.0%...

Reference manual CI status: - ❗ Reference manual CI will not be attempted unless your PR branches off the `nightly-with-manual` branch. Try `git rebase f9adafe54d5070acbd270643f71b8455ca8c8d68 --onto d3dda9f6d4428a906c096067ecb75e432afc4615`. You can force...