`rcases` doesn't clear original variable for `Quot`

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 rcases with quotients, the variable is not cleared. This contrasts the behavior for inductive types, where the discriminant is always cleared.

Context

Proving things about a quotient type

Steps to Reproduce

/--
error: unsolved goals
case mk
x✝ : Quot fun x x_1 => True
x : Nat
⊢ True
-/
#guard_msgs in
example (x : Quot fun _ _ : Nat => True) : True := by
  rcases x with ⟨x⟩

Expected behavior: Only one x variable remains, which should be x : Nat.

Actual behavior: The original variable is not cleared, keeping x✝ unnecessarily in the local context.

Versions

Lean 4.30.0-nightly-2026-03-11

Impact

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

Start with the minimal rcases reproducer in the issue and run it against the specified Lean nightly version. Trace the rcases handling for quotient types, comparing it with inductive-type handling. Done means the original Quot variable is cleared and only the expected x : Nat remains in the local context.