perf: detect unnecessary repeated checks in more situations

[hargoniX]

This PR improves on #11020 to remove even more unnecessary checks

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 1353298 against e76bbef are in! @hargoniX

Runs (2)

• other exited with code 2 (🟥)
• stdlib exited with code 2 (🟥)

[hargoniX]

Well clearly that's no good, time to investigate after vacation :D

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for cc72ace against 27e5e21 are in! @hargoniX

Major changes (2)

• liasolver//instructions changed by +1.0% (🟥).
• simp_local//instructions changed by +1.4% (🟥).

Minor changes (12)

• bv_decide_rewriter.lean//instructions changed by -0.8% (✅).
• ilean roundtrip//instructions changed by +0.9% (🟥).
• lake build no-op//instructions changed by +0.6% (🟥).
• libleanshared.so//binary size changed by +0.6% (🟥).
• parser//instructions changed by -0.7% (✅).
• simp_bubblesort_256//instructions changed by +0.9% (🟥).
• simp_subexpr//instructions changed by +0.9% (🟥).
• stdlib size//bytes .ir changed by +0.4% (🟥).
• stdlib size//bytes .olean.private changed by -0.5% (✅).
• stdlib size//lines C changed by +0.3% (🟥).
• stdlib//instructions changed by -0.2% (✅).
• tests/compiler//sum binary sizes changed by +0.5% (🟥).

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for a27d665 against bef8574 are in! @hargoniX

Major changes (2)

• liasolver//instructions changed by +1.0% (🟥).
• simp_local//instructions changed by +1.4% (🟥).

Minor changes (13)

• bv_decide_realworld//instructions changed by -0.5% (✅).
• bv_decide_rewriter.lean//instructions changed by -0.8% (✅).
• ilean roundtrip//instructions changed by +0.9% (🟥).
• lake build no-op//instructions changed by +0.6% (🟥).
• libleanshared.so//binary size changed by +0.6% (🟥).
• parser//instructions changed by -0.7% (✅).
• simp_bubblesort_256//instructions changed by +1.0% (🟥).
• simp_subexpr//instructions changed by +0.9% (🟥).
• stdlib size//bytes .ir changed by +0.4% (🟥).
• stdlib size//bytes .olean.private changed by -0.5% (✅).
• stdlib size//lines C changed by +0.3% (🟥).
• stdlib//instructions changed by -0.2% (✅).
• tests/compiler//sum binary sizes changed by +0.5% (🟥).

[ghost]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bef8574b93cacb87c7e9804870341441346a64b5 --onto 8b575dcbf2a3b907044df2233a61b61003eeeb45. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-17 13:43:45)

[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 bef8574b93cacb87c7e9804870341441346a64b5 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-17 13:43:46)

[hargoniX]

Seems like this breaks reuse more than it helps :(