`unknown free variable` in the info-view with `rcases` patterns

[SnirBroshi]

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 tactics that accept an rcases-like pattern such as rcases/obtain/ext placing the cursor inside the pattern sometimes shows unknown free variable errors in the info view.

Context

Zulip: 1 2

Steps to Reproduce

example (h : ∃ a : Nat, (∃ b, a = b + 1) ∧ 0 ≤ a) : True := by
  rcases h with ⟨_, ⟨b, rfl⟩, put_your_cursor_here_and_look_at_the_infoview⟩
  trivial

Place the cursor in the middle of the identifier put_your_cursor_here_and_look_at_the_infoview

Expected behavior: The info view should show the state and the expected type

Actual behavior: The info view shows:
Error updating: Error fetching goals: Rpc error: InternalError: unknown free variable `_fvar.136`.

Versions

Lean 4.29.0-nightly-2026-02-05
Target: x86_64-unknown-linux-gnu

Additional Information

Impact

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