Change of fvar type without change of FVarId at `simp`

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

When simplifying fvars, simp uses applySimpResultToLocalDecl, which, if possible, replaces the type of the fvar with a defeq type without changing the FVarId. This may break caches.

@leodemoura This is the issue I mentioned earlier.

Versions

"4.15.0-nightly-2024-11-26" (current master)

Impact

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

Start with src/Lean/Meta/Tactic/Simp/Main.lean at applySimpResultToLocalDecl, then inspect the minimal reproducible test case from the issue and how simp updates local declarations. Done means resolving the fvar type change without the cache-breaking behavior described, with the test case passing against the current Lean code.