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
```lean4
#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.
