fix: apply rcases substitution before recording pattern info

[berberman]

This PR fixes a bug in the rcases-family tactics where the InfoView could give "unknown free variable" errors when the cursor was inside the pattern. It hoists applying the fvar substitution to give addTermInfo' and addLocalVarInfo the correct expression. Previously, the substitution only happened in rfl/typed/tuple/alternative branches, which caused stale free variables to be recorded in the info tree. Repeated applications in recursive cases like .paren should be fine, because the domain of fs should be old fvars and replacement exprs should only refer current-goal fvars, not old-domain fvars. Proof elaboration shouldn't be affected by this PR.

The fix was suggested by @kmill.

Closes #12369

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 030397785c997509dad40e3c17e8793de04ef1ef --onto 0a6c31520b2ebaa6e71227454b46ebfb4986ae7b. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-03 03:36:54)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 030397785c997509dad40e3c17e8793de04ef1ef --onto fe3c7394fd3acb1faecf6fc26f267eb22058fe66. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-03 22:58:35)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 030397785c997509dad40e3c17e8793de04ef1ef --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-05-03 03:36:56)

[kmill]

This change potentially affects the clears list, but it might take some work coming up with an example that shows any difference. In any case, Lean.Elab.Tactic.RCases.finish applies the FVarSubst, though I notice it's doing it non-recursively (that's might be another bug).

Here's at least a case that currently fails on the most recent release that you could add to your test file:

example (n m : Nat) (h : n = m) : True := by
  rcases n, h with ⟨_ | _, -⟩
                         --^ unknown free variable `_fvar.1009`
  sorry
  sorry

I suspect you may be able to come up with an example where - doesn't clear things if one of the previous patterns created FVarSubst entries.

It would be nice to have a test case for .alts too demonstrating the fix, to prevent any regressions in the future.

[berberman]

Thanks for your review. I think clears is OK with this change. Before this patch, - could record the original fvar, but finish maps every recorded clear target through the final FVarSubst, so previous substitutions were accounted for when clearing. Now - should record the current fvar instead, and fs.get in finish should be harmless for those.

Also I think a single fs.get should be enough, because FVarSubst maintains compositional substitutions: insert rewrites existing mapped values, and append preserves (s.append t).apply e = t.apply (s.apply e). So if a cleared variable is later replaced by a new fvar, fs.get gives current fvar which makes - work.

I've added more tests, though multi-branch .alts was not a failure before the patch.