Renaming a variable also renames another variable

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In the following code:

namespace Nat
  inductive AnInductive: Nat → Type where
  | OptionA: Nat → AnInductive zero
  | OptionB: Nat → AnInductive zero

  def AnInductive.foo (w0: AnInductive n): Nat :=
    match w0 with
    | OptionA natA => natA
    | OptionB natB => natB
end Nat

renaming the variable natA also renames the last occurence of natB.

Steps to Reproduce

Position your caret inside an occurence of variable natA and rename the variable (F2, then enter a new name).

I believe the same issue is also reproducible in https://live.lean-lang.org/, even though the online editor does not
allow renaming variables -- position your care inside the latter occurence of natA (the former only works some
of the time for me), and the highlighted variables will include the last occurence of natB

Expected behavior: Only the variable natA is renamed

Actual behavior: Renaming natA to eg. asdf results in:

    | OptionA asdf => asdf
    | OptionB natB => asdf

Versions

Lean: 4.4.0-rc1
OS: Ubuntu 22.04.4 LTS;
Also reproducible on https://live.lean-lang.org/ as of posting.

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 Lean example in the issue and reproduce the F2 rename operation, checking the highlighted occurrences of natA and natB. Trace the rename handling used by the editor or live environment; done means renaming natA changes only its two occurrences and leaves natB unchanged.