`subst` and `simp` reorder hypotheses when rewriting

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

When using subst or simp to rewrite at hypotheses, the order of the hypotheses changes.
The ones who had their type changed move to the bottom.
This can cause strange behavior, including reviving a hypothesis with a shadowed name which makes another hypothesis inaccessible.

Context

#lean4 > `subst` revives old hypotheses

Steps to Reproduce

example {a b : Nat} (ha : a = 37) (hb : b = 37) : b = a := by
  have h : a = 37 := ha
  have h : b = 37 := hb
  subst ha
  exact h

example {a b : Nat} (ha : a = 37) (hb : b = 37) : b = a := by
  have h : a = 37 := ha
  have h : b = 37 := hb
  simp [ha] at *
  exact h

Expected behavior: After subst or simp the order of the hypotheses should stay the same, and the above proofs should succeed.

Actual behavior: Both subst and simp revive the old h, causing the exact to fail. If you comment out the first have, the proofs succeed.

Versions

Lean 4.35.0-nightly-2026-08-31
Target: x86_64-unknown-linux-gnu Linux

Additional Information

rw performs as expected, so perhaps its rewriting logic could be used.

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 two minimal examples in the issue and compare the hypothesis ordering after subst and simp with the behavior of rw. Trace the rewriting paths for these tactics; done means hypothesis order is preserved and both examples succeed without reviving the shadowed h.