diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index fb0f5b8151..aa2b5a9d2f 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -420,7 +420,7 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
                         return { stx := (← oldCmd?), val := (← old.next[i]?) }
                     } }) do
                       elabCommand cmd
-                    reusedCmds := reusedCmds && oldCmd?.any (·.structRangeEqWithTraceReuse opts cmd)
+                    reusedCmds := reusedCmds && oldCmd?.any (·.eqWithInfoAndTraceReuse opts cmd)
               else
                 elabCommand stxNew
         | _ =>
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index ffc333adf5..b59cc73330 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -155,7 +155,7 @@ private def elabHeaders (views : Array DefView)
           -- headers and all previous bodies could be reused and this body syntax is unchanged, then
           -- we can reuse the result
           reuseBody := reuseBody &&
-            view.value.structRangeEqWithTraceReuse (← getOptions) old.bodyStx
+            view.value.eqWithInfoAndTraceReuse (← getOptions) old.bodyStx
           -- no syntax guard to store, we already did the necessary checks
           oldBodySnap? := guard reuseBody *> pure ⟨.missing, old.bodySnap⟩
           oldTacSnap? := do
@@ -977,7 +977,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
             -- blocking wait, `HeadersParsedSnapshot` (and hopefully others) should be quick
             let old ← old.val.get.toTyped? DefsParsedSnapshot
             let oldParsed ← old.defs[i]?
-            guard <| fullHeaderRef.structRangeEqWithTraceReuse opts oldParsed.fullHeaderRef
+            guard <| fullHeaderRef.eqWithInfoAndTraceReuse opts oldParsed.fullHeaderRef
             -- no syntax guard to store, we already did the necessary checks
             return ⟨.missing, oldParsed.headerProcessedSnap⟩
           new := headerPromise
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 317a9f749e..4bbdb2757e 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -333,7 +333,7 @@ instance : MonadBacktrack SavedState TermElabM where
 Manages reuse information for nested tactics by `split`ting given syntax into an outer and inner
 part. `act` is then run on the inner part but with reuse information adjusted as following:
 * If the old (from `tacSnap?`'s `SyntaxGuarded.stx`) and new (from `stx`) outer syntax are not
-  identical according to `Syntax.structRangeEq`, reuse is disabled.
+  identical according to `Syntax.eqWithInfo`, reuse is disabled.
 * Otherwise, the old syntax as stored in `tacSnap?` is updated to the old *inner* syntax.
 * In any case, we also use `withRef` on the inner syntax to avoid leakage of the outer syntax into
   `act` via this route.
@@ -349,7 +349,7 @@ def withNarrowedTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithRead
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
     { tacSnap with old? := tacSnap.old?.bind fun old => do
       let (oldOuter, oldInner) := split old.stx
-      guard <| outer.structRangeEqWithTraceReuse opts oldOuter
+      guard <| outer.eqWithInfoAndTraceReuse opts oldOuter
       return { old with stx := oldInner }
     }
   }) do
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 06c09e16d2..a64999dd0b 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -33,6 +33,8 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
 def SourceInfo.getRange? (canonicalOnly := false) (info : SourceInfo) : Option String.Range :=
   return ⟨(← info.getPos? canonicalOnly), (← info.getTailPos? canonicalOnly)⟩
 
+deriving instance BEq for SourceInfo
+
 /-! # Syntax AST -/
 
 inductive IsNode : Syntax → Prop where
@@ -84,9 +86,11 @@ end SyntaxNode
 namespace Syntax
 
 /--
-Compare syntax structures and position ranges, but not whitespace.
-We generally assume that if syntax trees equal in this way generate the same elaboration output,
-including positions contained in e.g. diagnostics and the info tree.
+Compares syntax structures and position ranges, but not whitespace. We generally assume that if
+syntax trees equal in this way generate the same elaboration output, including positions contained
+in e.g. diagnostics and the info tree. However, as we have a few request handlers such as `goalsAt?`
+that are sensitive to whitespace information in the info tree, we currently use `eqWithInfo` instead
+for reuse checks.
 -/
 partial def structRangeEq : Syntax → Syntax → Bool
   | .missing, .missing => true
@@ -111,6 +115,30 @@ def structRangeEqWithTraceReuse (opts : Options) (stx1 stx2 : Syntax) : Bool :=
     else
       false
 
+
+/-- Full comparison of syntax structures and source infos.  -/
+partial def eqWithInfo : Syntax → Syntax → Bool
+  | .missing, .missing => true
+  | .node info k args, .node info' k' args' =>
+    info == info' && k == k' && args.isEqv args' eqWithInfo
+  | .atom info val, .atom info' val' => info == info' && val == val'
+  | .ident info rawVal val preresolved, .ident info' rawVal' val' preresolved' =>
+    info == info' && rawVal == rawVal' && val == val' && preresolved == preresolved'
+  | _, _ => false
+
+/-- Like `eqWithInfo` but prints trace on failure if `trace.Elab.reuse` is activated. -/
+def eqWithInfoAndTraceReuse (opts : Options) (stx1 stx2 : Syntax) : Bool :=
+  if stx1.eqWithInfo stx2 then
+    true
+  else
+    if opts.getBool `trace.Elab.reuse then
+      dbg_trace "reuse stopped:
+{stx1.formatStx (showInfo := true)} !=
+{stx2.formatStx (showInfo := true)}"
+      false
+    else
+      false
+
 def getAtomVal : Syntax → String
   | atom _ val => val
   | _          => ""
diff --git a/tests/lean/interactive/incrementalTactic.lean b/tests/lean/interactive/incrementalTactic.lean
index e5e153eeed..25aa68e46e 100644
--- a/tests/lean/interactive/incrementalTactic.lean
+++ b/tests/lean/interactive/incrementalTactic.lean
@@ -11,6 +11,10 @@ def basic : True := by
               --^ sync
               --^ insert: ".5"
 
+/-!
+Ideally trailing whitespace should be ignored. CURRENTLY NOT WORKING as we use `Syntax.eqWithInfo`;
+we will need to patch old syntax info stored in the info tree to go back to `Syntax.structRangeEq`.
+-/
 -- RESET
 def trailingWhitespace : True := by
   dbg_trace "t 0"
@@ -51,3 +55,19 @@ def strayToken : True := by
   unfold f
         --^ sync
         --^ insert: " -"
+
+/-!
+Insufficient reuse checking of trailing whitespace info in the info tree led to the goal view
+showing multiple tactics as they all claimed to be at the end of the file (which they were in prior
+versions).
+-/
+-- RESET
+def dup_goals : True := by
+  show True
+--^ sync
+--^ insert: "show True\n  show True\n  show True\n  show True\n  "
+
+--^ sync
+--^ goals
+-- (note that request positions are computed relative to the original document, so the checks above
+-- will point at a `show` at run time)
diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out
index 6b79256e2c..9417b2fa17 100644
--- a/tests/lean/interactive/incrementalTactic.lean.expected.out
+++ b/tests/lean/interactive/incrementalTactic.lean.expected.out
@@ -5,6 +5,7 @@ b 2.5
 t 0
 t 1
 t 2
+t 2
 {"version": 3,
  "uri": "file:///incrementalTactic.lean",
  "diagnostics":
@@ -54,3 +55,10 @@ t 2
    {"start": {"line": 3, "character": 9},
     "end": {"line": 3, "character": 16}}}]}
 s
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", diffStatus? := none }
+                         (Lean.Widget.TaggedText.text "True"),
+               isInserted? := some false,
+               isRemoved? := none,
+               hyps := #[] }] }
+