diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 12ebca9e7b8d..23a744a9ff11 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -628,7 +628,7 @@ mutual
           (in particular, `Lean.Elab.Term.withReuseContext`) controls the ref to avoid leakage of outside data.
           Note that `tacticSyntax` contains no position information itself, since it is erased by `Lean.Elab.Term.quoteAutoTactic`.
           -/
-          let info := (← getRef).getHeadInfo
+          let info := (← getRef).getHeadInfo.nonCanonicalSynthetic
           let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info)
           let mvar ← mkTacticMVar argType.consumeTypeAnnotations tacticBlock (.autoParam argName)
           -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`.
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 6332ead08c82..91872d4831e2 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -853,7 +853,7 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt
               let stx ← `(by $tacticSyntax)
               -- See comment in `Lean.Elab.Term.ElabAppArgs.processExplicitArg` about `tacticSyntax`.
               -- We add info to get reliable positions for messages from evaluating the tactic script.
-              let info := field.ref.getHeadInfo
+              let info := field.ref.getHeadInfo.nonCanonicalSynthetic
               let stx := stx.raw.rewriteBottomUp (·.setInfo info)
               let type := (d.getArg! 0).consumeTypeAnnotations
               let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName)
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 6e487ff0e8d4..ffd369190226 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -33,6 +33,16 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
 def SourceInfo.getRange? (canonicalOnly := false) (info : SourceInfo) : Option String.Range :=
   return ⟨(← info.getPos? canonicalOnly), (← info.getTailPos? canonicalOnly)⟩
 
+/--
+Converts an `original` or `synthetic (canonical := true)` `SourceInfo` to a
+`synthetic (canonical := false)` `SourceInfo`.
+This is sometimes useful when `SourceInfo` is being moved around between `Syntax`es.
+-/
+def SourceInfo.nonCanonicalSynthetic : SourceInfo → SourceInfo
+  | SourceInfo.original _ pos _ endPos => SourceInfo.synthetic pos endPos false
+  | SourceInfo.synthetic pos endPos _  => SourceInfo.synthetic pos endPos false
+  | SourceInfo.none                    => SourceInfo.none
+
 deriving instance BEq for SourceInfo
 
 /-! # Syntax AST -/
diff --git a/tests/lean/interactive/ghostGoals.lean b/tests/lean/interactive/ghostGoals.lean
new file mode 100644
index 000000000000..bab4ded2af73
--- /dev/null
+++ b/tests/lean/interactive/ghostGoals.lean
@@ -0,0 +1,19 @@
+-- Issue originally reported at
+-- https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/tactic.20doesn't.20change.20primary.20goal.20state/near/488957772
+class Preorder (α : Type) extends LE α, LT α where
+  le_refl : ∀ a : α, a ≤ a
+  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
+  lt := fun a b => a ≤ b ∧ ¬b ≤ a
+  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
+
+class PartialOrder (α : Type) extends Preorder α where
+  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
+
+instance : PartialOrder Nat where
+  le := (· ≤ ·)
+  le_refl := Nat.le_refl
+  le_trans a b c := Nat.le_trans
+  le_antisymm := by
+    intro x
+      -- One goal: x : Nat ⊢ ∀ (b : Nat), x ≤ b → b ≤ x → x = b
+  --^ $/lean/plainGoal
diff --git a/tests/lean/interactive/ghostGoals.lean.expected.out b/tests/lean/interactive/ghostGoals.lean.expected.out
new file mode 100644
index 000000000000..9a7516752d0c
--- /dev/null
+++ b/tests/lean/interactive/ghostGoals.lean.expected.out
@@ -0,0 +1,4 @@
+{"textDocument": {"uri": "file:///ghostGoals.lean"},
+ "position": {"line": 17, "character": 4}}
+{"rendered": "```lean\nx : Nat\n⊢ ∀ (b : Nat), x ≤ b → b ≤ x → x = b\n```",
+ "goals": ["x : Nat\n⊢ ∀ (b : Nat), x ≤ b → b ≤ x → x = b"]}