fix: apply rcases substitution before recording pattern info

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)

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

tests/server_interactive/12369.lean

@@ -0,0 +1,32 @@
+/-!
+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
+
+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

tests/server_interactive/12369.lean.out.expected

@@ -0,0 +1,31 @@
+{"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"]}
+{"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"]}