VS Code F2 renaming goes too far

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

VS Code F2 renaming renames more than it should

Steps to Reproduce

1. Open the following in VS Code

import Mathlib.Algebra.Lie.Nilpotent

universe u₁ u₂ u₃ u₄

variable {R : Type u₁} {L : Type u₂} {M : Type u₄}
variable [CommRing R] [LieRing L] [LieAlgebra R L]
variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]

namespace LieSubmodule

open LieModule

variable {I : LieIdeal R L} {x : L}

theorem exists_smul_add_of_span_sup_eq_top (y : L) : ∃ t : R, ∃ z ∈ I, y = t • x + z := by
  sorry

theorem lie_top_eq_of_span_sup_eq_top (N : LieSubmodule R L M) :
    (↑⁅(⊤ : LieIdeal R L), N⁆ : Submodule R M) =
      (N : Submodule R M).map (toEnd R L M x) ⊔ (↑⁅I, N⁆ : Submodule R M) := by
  sorry

end LieSubmodule

2. Select the variable R on line 5
3. Use VS Code F2 feature to rename

Expected behavior: Only the variable R should be renamed.

Actual behavior: The variable R and also the variable y appearing in y = t • x + z is renamed.

Versions

Lean: 4.26.0-rc2
OS: MacOS 15.6.1

Reproduce the F2 rename from the provided Lean snippet in VS Code, first reducing it to a minimal case without Mathlib or Batteries. Trace the F2 rename entry point and verify that renaming variable R changes only R, while the y in y = t • x + z remains unchanged.