`simp` fails to rewrite in match discriminants with hypotheses

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

simp fails to rewrite discriminants of match expressions if they have hypotheses associated to them.

Context

I worked around this problem in #8210 and this came up again in https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.E2.9C.94.20Telling.20split.20where.20to.20split/with/523303521

Steps to Reproduce

example (h : x = 1) :
    (match _ : x with
    | 0 => 0
    | _ + 1 => 0) = 0 := by
  simp [h]

Expected behavior: simp should be able to rewrite the discriminant and solve the goal.

Actual behavior: simp fails to rewrite the discriminant.

Versions

Lean 4.21.0-nightly-2025-06-09

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 from the issue against the Lean nightly release and inspect the simp handling of match discriminants carrying hypotheses. The work is done when the shown simp [h] example rewrites the discriminant and closes the goal as expected.