`rw` tactic "steals" goals (again)

Prerequisites

• 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

Consider this code:

example {l : List Nat} {P : Prop} {l' l'' : P → List Nat} {a : Nat}
    (hl : (hp : P) → l = a :: l' hp) (hl' : (hp : P) → l' hp = l'' hp) (h : P) :
    l = a :: l'' h := by
  rw [hl]
  · sorry
  · sorry

After the rw, there are two goals: a :: l' ?m.7 = a :: l'' h and P. Now, if I replace the first sorry with rw [hl'], the second goal disappears:

example {l : List Nat} {P : Prop} {l' l'' : P → List Nat} {a : Nat}
    (hl : (hp : P) → l = a :: l' hp) (hl' : (hp : P) → l' hp = l'' hp) (h : P) :
    l = a :: l'' h := by
  rw [hl]
  · rw [hl']
  · sorry -- No goals to be solved

Context

This is the same issue as #10172, just with a different reproducer that is still broken after the fix for the earlier issue.

Expected behavior: rw [hl'] should close the first branch and leave the second branch open.

Actual behavior: Second goal disappears.

Versions

Lean 4.28.0-nightly-2026-01-23
Target: x86_64-unknown-linux-gnu

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 minimal reproducer against the specified Lean nightly and inspect the rw tactic behavior after the first rewrite. Trace how the two goals from rw [hl] are managed when rw [hl'] closes the first branch; done means the second P goal remains open, with a regression test covering this case.