diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 0d9514ae77..0253c5df6f 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -4170,6 +4170,16 @@ def withRef [Monad m] [MonadRef m] {α} (ref : Syntax) (x : m α) : m α :=
   let ref := replaceRef ref oldRef
   MonadRef.withRef ref x
 
+/--
+If `ref? = some ref`, run `x : m α` with a modified value for the `ref` by calling `withRef`.
+Otherwise, run `x` directly.
+-/
+@[always_inline, inline]
+def withRef? [Monad m] [MonadRef m] {α} (ref? : Option Syntax) (x : m α) : m α :=
+  match ref? with
+  | some ref => withRef ref x
+  | _        => x
+
 /-- A monad that supports syntax quotations. Syntax quotations (in term
     position) are monadic values that when executed retrieve the current "macro
     scope" from the monad and apply it to every identifier they introduce
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index aa02a0f849..72c5d139c4 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -362,9 +362,9 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   | `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*))
   | _ => throwUnsupportedSyntax
 where
-  introStep (ref : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do
+  introStep (ref? : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do
     let fvarId ← liftMetaTacticAux fun mvarId => do
-      let (fvarId, mvarId) ← mvarId.intro n
+      let (fvarId, mvarId) ← withRef? ref? <| mvarId.intro n
       pure (fvarId, [mvarId])
     if let some typeStx := typeStx? then
       withMainContext do
@@ -374,9 +374,9 @@ where
         unless (← isDefEqGuarded type fvarType) do
           throwError "type mismatch at `intro {fvar}`{← mkHasTypeButIsExpectedMsg fvarType type}"
         liftMetaTactic fun mvarId => return [← mvarId.replaceLocalDeclDefEq fvarId type]
-    if let some stx := ref then
+    if let some ref := ref? then
       withMainContext do
-        Term.addLocalVarInfo stx (mkFVar fvarId)
+        Term.addLocalVarInfo ref (mkFVar fvarId)
 
 @[builtin_tactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do
   let matchAlts := stx[1]
diff --git a/src/Lean/Elab/Tactic/RCases.lean b/src/Lean/Elab/Tactic/RCases.lean
index d8ecac3b21..31d3ecac71 100644
--- a/src/Lean/Elab/Tactic/RCases.lean
+++ b/src/Lean/Elab/Tactic/RCases.lean
@@ -507,7 +507,7 @@ partial def rintroCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (a
   match pat with
   | `(rintroPat| $pat:rcasesPat) =>
     let pat := (← RCasesPatt.parse pat).typed? ref ty?
-    let (v, g) ← g.intro (pat.name?.getD `_)
+    let (v, g) ← withRef pat.ref <| g.intro (pat.name?.getD `_)
     rcasesCore g fs clears (.fvar v) a pat cont
   | `(rintroPat| ($(pats)* $[: $ty?']?)) =>
     let ref := if pats.size == 1 then pat.raw else .missing
diff --git a/tests/lean/interactive/5659.lean b/tests/lean/interactive/5659.lean
new file mode 100644
index 0000000000..92b03237bf
--- /dev/null
+++ b/tests/lean/interactive/5659.lean
@@ -0,0 +1,13 @@
+/-!
+  # `rintro` and `intro` error message should point to excess arg
+
+  Below, the errors should point to `h` because there is no lambda it binds.
+  The error should not point to `hn`; it would be OKish to underline the whole line. -/
+
+example : (∃ n : Nat, n < 0) → False := by
+  rintro ⟨n, hn⟩ h
+              --^ collectDiagnostics
+
+example : (∃ n : Nat, n < 0) → False := by
+  intro ⟨n, hn⟩ h
+             --^ collectDiagnostics
diff --git a/tests/lean/interactive/5659.lean.expected.out b/tests/lean/interactive/5659.lean.expected.out
new file mode 100644
index 0000000000..95178ac230
--- /dev/null
+++ b/tests/lean/interactive/5659.lean.expected.out
@@ -0,0 +1,22 @@
+{"version": 1,
+ "uri": "file:///5659.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 7, "character": 17}, "end": {"line": 7, "character": 18}},
+   "message":
+   "tactic 'introN' failed, insufficient number of binders\ncase intro\nn : Nat\nhn : n < 0\n⊢ False",
+   "fullRange":
+   {"start": {"line": 7, "character": 17},
+    "end": {"line": 7, "character": 18}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 11, "character": 16},
+    "end": {"line": 11, "character": 17}},
+   "message":
+   "tactic 'introN' failed, insufficient number of binders\nn : Nat\nhn : n < 0\n⊢ False",
+   "fullRange":
+   {"start": {"line": 11, "character": 16},
+    "end": {"line": 11, "character": 17}}}]}
diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out
index 706ae32c68..b429e40063 100644
--- a/tests/lean/interactive/incrementalTactic.lean.expected.out
+++ b/tests/lean/interactive/incrementalTactic.lean.expected.out
@@ -12,11 +12,12 @@ t 2
  [{"source": "Lean 4",
    "severity": 1,
    "range":
-   {"start": {"line": 4, "character": 4}, "end": {"line": 4, "character": 13}},
+   {"start": {"line": 4, "character": 12}, "end": {"line": 4, "character": 13}},
    "message":
    "tactic 'introN' failed, insufficient number of binders\na n : Nat\n⊢ True",
    "fullRange":
-   {"start": {"line": 4, "character": 4}, "end": {"line": 4, "character": 13}}},
+   {"start": {"line": 4, "character": 12},
+    "end": {"line": 4, "character": 13}}},
   {"source": "Lean 4",
    "severity": 1,
    "range":