`rw [def]` only works with first applicable equation lemma

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When using rw to unfold a recursive definition using equation lemmas, it seems to find the first equation lemma whose LHS appears in the goal, and then find the leftmost occurrence of that LHS in the goal. I would've expected it to find the leftmost subexpression in the goal which matches any of the possible equation lemmas. Similarly, I would expect nth_rw n (AKA rw (config := {occs := .pos [n]})) to find the nth subexpression which matches any of the equation lemmas, not just the first equation lemma.

Context

I first noticed then when a new user was confused by it on Zulip. Then I opened a Zulip thread.

Steps to Reproduce

example (x : α) : [x].length = ([] : List α).length + 1 := by
  rw [List.length] -- unsolved goals; rewrites `[].length = 0` instead of `[x].length = [].length + 1`
  -- expected: solves goal because `rw` applies to leftmost applicable subexpression which is `[x].length`

example (x : α) : [x].length = ([] : List α).length + 1 := by
  rw (config := {occs := .pos [1]}) [List.length] -- error: same as above
  -- expected: same as above

example (x : α) : [x].length = ([] : List α).length + 1 := by
  rw (config := {occs := .pos [2]}) [List.length] -- error; `rw` can't find a second occurence for the `[].length = _` equation
  -- expected: new goal is `⊢ [x].length = 0 + 1`

-- Workaround: Use the specific desired equation lemma
example (x : α) : [x].length = ([] : List α).length + 1 := by
  rw [List.length.eq_2] -- success

Versions

4.12.0-nightly-2024-08-13
live.lean-lang.org

Impact

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

Run the minimal reproducer with rw [List.length] and both nth_rw configurations to observe the current behavior. Trace the rw and nth_rw entry points, then verify that matching considers all applicable equation lemmas and occurrence positions, including the List.length.eq_2 workaround cases.