fix: prevent a hang in acLt

[eric-wieser]

This PR removes some cases where simp would significantly overrun a timeout.

This is a little tricky to test cleanly; using mathlib's #count_heartbeats as

#count_heartbeats in
set_option maxHeartbeats 200000 in
example (k : Nat) (a : Fin (1 + k + 1) → Nat) :
    0 ≤ sumRange (1 + k + 1) (fun i =>
        if h : i < 1 + k + 1 then a ⟨i, h⟩ else 0) := by
  simp only [Nat.add_comm, sumRange_add]

I see 200010 heartbeats with this PR, and 1873870 (9x the requested limit) without.

This type of failure is wasteful in AI systems which try tactics with a short timeout.

[eric-wieser]

changelog-language

[Rob23oba]

!bench

[leanprover-radar]

Benchmark results for d5cf7d7 against d53b46a are in. There are no significant changes. @Rob23oba

• 🟥 build//instructions: +3.5G (+0.03%)

Medium changes (2🟥)

• 🟥 build/module/Init.Data.Nat.Linear//instructions: +2.8G (+5.09%)
• 🟥 build/module/Init.Data.Nat.SOM//instructions: +1.3G (+6.77%)

Small changes (2🟥)

• 🟥 build/module/Init.Grind.AC//instructions: +178.8M (+1.68%)
• 🟥 build/module/Lean.Meta.ACLt//instructions: +17.3M (+0.84%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d53b46a0f3a7d0822550f4179ca3dab446a3c448 --onto e0a29f43d2e4685febd0ed6bcfad511f7a235b6f. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-10 19:26:16)

[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 d53b46a0f3a7d0822550f4179ca3dab446a3c448 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-10 19:26:18)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-10 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. (2026-04-10 21:51:02)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13367 has successfully built against this PR. (2026-04-10 22:48:00) View Log