From 5629ac2e7ef90caf91aa17556113ca9b739ba233 Mon Sep 17 00:00:00 2001
From: Potato Hatsue <1793913507@qq.com>
Date: Sat, 2 May 2026 18:38:57 -0700
Subject: [PATCH 1/2] fix: apply `rcases` substitution before recording pattern
 info

This PR hoists `fs.apply` to let `addTermInfo'` and `addLocalVarInfo` use correct expr.
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.
---
 src/Lean/Elab/Tactic/RCases.lean              |  5 ++---
 tests/server_interactive/12369.lean           | 19 +++++++++++++++++++
 .../12369.lean.out.expected                   | 12 ++++++++++++
 3 files changed, 33 insertions(+), 3 deletions(-)
 create mode 100644 tests/server_interactive/12369.lean
 create mode 100644 tests/server_interactive/12369.lean.out.expected

diff --git a/src/Lean/Elab/Tactic/RCases.lean b/src/Lean/Elab/Tactic/RCases.lean
index bfad9f98be01..e1fda580b910 100644
--- a/src/Lean/Elab/Tactic/RCases.lean
+++ b/src/Lean/Elab/Tactic/RCases.lean
@@ -273,12 +273,13 @@ partial def rcasesCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (e
   let asFVar : Expr → MetaM _
     | .fvar e => pure e
     | e => throwError "Tactic `rcases` failed: `{e}` is not a free variable"
+  let e := fs.apply e
   withRef pat.ref <| g.withContext do match pat with
   | .one ref `rfl =>
     Term.synthesizeSyntheticMVarsNoPostponing
     -- Note: the mdata prevents the span from getting highlighted like a variable
     Term.addTermInfo' ref (.mdata {} e)
-    let (fs, g) ← substEq g (← asFVar (fs.apply e)) fs
+    let (fs, g) ← substEq g (← asFVar e) fs
     cont g fs clears a
   | .one ref _ =>
     if e.isFVar then
@@ -290,7 +291,6 @@ partial def rcasesCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (e
   | .typed ref pat ty =>
     Term.addTermInfo' ref (.mdata {} e)
     let expected ← Term.elabType ty
-    let e := fs.apply e
     let etype ← inferType e
     unless ← isDefEq etype expected do
       Term.throwTypeMismatchError "Tactic `rcases` failed: scrutinee" expected etype e
@@ -302,7 +302,6 @@ partial def rcasesCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (e
     rcasesCore g fs clears e a p cont
   | _ =>
     Term.addTermInfo' pat.ref (.mdata {} e)
-    let e := fs.apply e
     let _ ← asFVar e
     Term.synthesizeSyntheticMVarsNoPostponing
     let type ← whnfD (← inferType e)
diff --git a/tests/server_interactive/12369.lean b/tests/server_interactive/12369.lean
new file mode 100644
index 000000000000..2508a8517e4f
--- /dev/null
+++ b/tests/server_interactive/12369.lean
@@ -0,0 +1,19 @@
+/-!
+After an `rcases`-style `rfl` pattern substitutes a variable,
+info view on later patterns should use the substituted local hypothesis, not an old free variable.
+-/
+
+example (h : ∃ a : Nat, (∃ b, a = b + 1) ∧ 0 ≤ a) : True := by
+  rcases h with ⟨_, ⟨b, rfl⟩, hle⟩
+                           --^ $/lean/plainGoal
+  trivial
+
+example : (∃ a : Nat, (∃ b, a = b + 1) ∧ 0 ≤ a) → True := by
+  rintro ⟨_, ⟨b, rfl⟩, hle⟩
+                    --^ $/lean/plainGoal
+  trivial
+
+example (h : ∃ a : Nat, (∃ b, a = b + 1) ∧ 0 ≤ a) : True := by
+  obtain ⟨_, ⟨b, rfl⟩, (hle)⟩ := h
+                     --^ $/lean/plainGoal
+  trivial
diff --git a/tests/server_interactive/12369.lean.out.expected b/tests/server_interactive/12369.lean.out.expected
new file mode 100644
index 000000000000..0b8d95d38a24
--- /dev/null
+++ b/tests/server_interactive/12369.lean.out.expected
@@ -0,0 +1,12 @@
+{"textDocument": {"uri": "file:///12369.lean"},
+ "position": {"line": 6, "character": 29}}
+{"rendered": "```lean\nb : Nat\nhle : 0 ≤ b + 1\n⊢ True\n```",
+ "goals": ["b : Nat\nhle : 0 ≤ b + 1\n⊢ True"]}
+{"textDocument": {"uri": "file:///12369.lean"},
+ "position": {"line": 11, "character": 22}}
+{"rendered": "```lean\nb : Nat\nhle : 0 ≤ b + 1\n⊢ True\n```",
+ "goals": ["b : Nat\nhle : 0 ≤ b + 1\n⊢ True"]}
+{"textDocument": {"uri": "file:///12369.lean"},
+ "position": {"line": 16, "character": 23}}
+{"rendered": "```lean\nb : Nat\nhle : 0 ≤ b + 1\n⊢ True\n```",
+ "goals": ["b : Nat\nhle : 0 ≤ b + 1\n⊢ True"]}

From e282f23a509e1977b0fae9cda49b64d2915c3180 Mon Sep 17 00:00:00 2001
From: Potato Hatsue <1793913507@qq.com>
Date: Sun, 3 May 2026 14:43:13 -0700
Subject: [PATCH 2/2] Update tests

---
 tests/elab/rcases.lean                        |  5 +++++
 tests/server_interactive/12369.lean           | 13 +++++++++++++
 .../12369.lean.out.expected                   | 19 +++++++++++++++++++
 3 files changed, 37 insertions(+)

diff --git a/tests/elab/rcases.lean b/tests/elab/rcases.lean
index 263720da04ce..e672ee9887ac 100644
--- a/tests/elab/rcases.lean
+++ b/tests/elab/rcases.lean
@@ -209,3 +209,8 @@ example (b c : Nat) : True := by
   obtain h : b = c ^ 2 := test_sorry
   subst h
   trivial
+
+example (a b : Nat) (h : 0 ≤ a ∧ b = a) : True := by
+  rcases h with ⟨-, rfl⟩
+  fail_if_success have : 0 ≤ b := by assumption
+  trivial
diff --git a/tests/server_interactive/12369.lean b/tests/server_interactive/12369.lean
index 2508a8517e4f..e426c3e96903 100644
--- a/tests/server_interactive/12369.lean
+++ b/tests/server_interactive/12369.lean
@@ -17,3 +17,16 @@ example (h : ∃ a : Nat, (∃ b, a = b + 1) ∧ 0 ≤ a) : True := by
   obtain ⟨_, ⟨b, rfl⟩, (hle)⟩ := h
                      --^ $/lean/plainGoal
   trivial
+
+example (n m : Nat) (h : n = m) : True := by
+  rcases n, h with ⟨_ | _, -⟩
+                         --^ $/lean/plainGoal
+  trivial
+  trivial
+
+example (h : ∃ a : Nat, (∃ b, a = b + 1) ∧ (a = 1 ∨ a = 2)) : True := by
+  rcases h with ⟨_, ⟨b, rfl⟩, h1 | h2⟩
+                            --^ $/lean/plainGoal
+                                 --^ $/lean/plainGoal
+  trivial
+  trivial
diff --git a/tests/server_interactive/12369.lean.out.expected b/tests/server_interactive/12369.lean.out.expected
index 0b8d95d38a24..ef9e1df68ef6 100644
--- a/tests/server_interactive/12369.lean.out.expected
+++ b/tests/server_interactive/12369.lean.out.expected
@@ -10,3 +10,22 @@
  "position": {"line": 16, "character": 23}}
 {"rendered": "```lean\nb : Nat\nhle : 0 ≤ b + 1\n⊢ True\n```",
  "goals": ["b : Nat\nhle : 0 ≤ b + 1\n⊢ True"]}
+{"textDocument": {"uri": "file:///12369.lean"},
+ "position": {"line": 21, "character": 27}}
+{"rendered":
+ "```lean\ncase zero\nm : Nat\n⊢ True\n```\n---\n```lean\ncase succ\nm n✝ : Nat\n⊢ True\n```",
+ "goals": ["case zero\nm : Nat\n⊢ True", "case succ\nm n✝ : Nat\n⊢ True"]}
+{"textDocument": {"uri": "file:///12369.lean"},
+ "position": {"line": 27, "character": 30}}
+{"rendered":
+ "```lean\ncase inl\nb : Nat\nh1 : b + 1 = 1\n⊢ True\n```\n---\n```lean\ncase inr\nb : Nat\nh2 : b + 1 = 2\n⊢ True\n```",
+ "goals":
+ ["case inl\nb : Nat\nh1 : b + 1 = 1\n⊢ True",
+  "case inr\nb : Nat\nh2 : b + 1 = 2\n⊢ True"]}
+{"textDocument": {"uri": "file:///12369.lean"},
+ "position": {"line": 27, "character": 35}}
+{"rendered":
+ "```lean\ncase inl\nb : Nat\nh1 : b + 1 = 1\n⊢ True\n```\n---\n```lean\ncase inr\nb : Nat\nh2 : b + 1 = 2\n⊢ True\n```",
+ "goals":
+ ["case inl\nb : Nat\nh1 : b + 1 = 1\n⊢ True",
+  "case inr\nb : Nat\nh2 : b + 1 = 2\n⊢ True"]}