"Rename symbol" does not work with `generalize`

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

The "Rename symbol" operation in vscode does not see through the generalize tactic

Context

This came up while investigating things similar to #metaprogramming / tactics > Persisting hypotheses across tactics @ 💬

Steps to Reproduce

1. Run the following code

   example (x : Nat) (hx : (x + x) + (x + x) = 2) : x + x = 1 := by
     generalize h : x + x = y at *
     let p := hx
     sorry
   

2. Put your cursor on the first hx
3. Run "Rename symbol" in vscode, and type hx2

Expected behavior: Both hxs change to hx2, and the proof keeps working.

Actual behavior: Only the first one changes, and the proof breaks.

Versions

Lean 4.23.0-nightly-2025-07-16
Target: x86_64-unknown-linux-gnu

Additional Information

Modifying the tactic to record ofFVarAliasInfos fixes this, but there is some disagreement over whether this is a correct use of this feature.

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 failure through VSCode's "Rename symbol" operation. Trace how the generalize tactic handles the aliased hypothesis and inspect the mentioned ofFVarAliasInfos behavior. Done means renaming either hx updates both occurrences and the proof continues to work.