`simp_all` makes further progress on second invocation

Description

Sometimes simp_all makes further progress on a second invocation.

Context

I encountered this while doing simp lemma confluence testing with @nomeata's tool.

Steps to Reproduce

open List

@[simp] theorem range'_head (n : Nat) (h) : (range' s n).head h = s := by
  sorry

example (s n : Nat) (h : range' s n ≠ []) : s ≤ (List.range' s n).head h ∧ (List.range' s n).head h < s + n := by
  simp_all
  simp_all
  omega

Expected behavior:

The first simp_all should already have done what the second simp_all goes on to do, so the second simp_all should error.

Actual behavior:

Proof succeeds, making progress at both simp_alls

Versions

v4.11.0-rc2, and nightly-2024-08-19

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the provided simp_all reproduction on the reported Lean versions and compare the first and second invocations. Done means the first invocation makes all available progress so the second simp_all reports no further progress, while the proof's final omega step remains appropriate.