diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index 78d2490bdf..9952cf4269 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -14,10 +14,6 @@ def toMonad [Monad m] [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[macroInline] def getD : Option α → α → α
-  | some x, _ => x
-  | none,   e => e
-
 @[inline] def toBool : Option α → Bool
   | some _ => true
   | none   => false
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 28fee3ba78..33939a1e12 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -260,9 +260,6 @@ end Syntax
   | none => x
   | some ref => withRef ref x
 
-def mkAtom (val : String) : Syntax :=
-  Syntax.atom SourceInfo.none val
-
 @[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
   Syntax.node k args
 
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 1568078ece..685cdb7096 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -252,21 +252,20 @@ syntax (name := erewriteSeq) "erewrite " rwRuleSeq (location)? : tactic
 syntax (name := rwSeq) "rw " rwRuleSeq (location)? : tactic
 syntax (name := erwSeq) "erw " rwRuleSeq (location)? : tactic
 
-private def withCheapRefl (tac : Syntax) : MacroM Syntax :=
-  `(tactic| $tac; try (withReducible rfl))
+def rwWithRfl (kind : SyntaxNodeKind) (atom : String) (stx : Syntax) : MacroM Syntax := do
+  -- We show the `rfl` state on `]`
+  let seq   := stx[1]
+  let rbrak := seq[2]
+  -- Replace `]` token with one without position information in the expanded tactic
+  let seq   := seq.setArg 2 (mkAtom "]")
+  let tac   := stx.setKind kind |>.setArg 0 (mkAtomFrom stx atom) |>.setArg 1 seq
+  `(tactic| $tac; try (withReducible rfl%$rbrak))
 
-@[macro rwSeq]
-def expandRwSeq : Macro := fun stx =>
-  let rbrak := stx[1][2]
-  -- show "cheap refl" state on `]`
-  withRef rbrak <|
-    withCheapRefl (stx.setKind `Lean.Parser.Tactic.rewriteSeq |>.setArg 0 (mkAtomFrom stx "rewrite"))
+@[macro rwSeq] def expandRwSeq : Macro :=
+  rwWithRfl ``Lean.Parser.Tactic.rewriteSeq "rewrite"
 
-@[macro erwSeq]
-def expandERwSeq : Macro := fun stx =>
-  let rbrak := stx[1][2]
-  withRef rbrak <|
-    withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite"))
+@[macro erwSeq] def expandERwSeq : Macro :=
+  rwWithRfl ``Lean.Parser.Tactic.erewriteSeq "erewrite"
 
 syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
 
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 95c4f700c6..2bd1798890 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -981,6 +981,10 @@ export Option (none some)
 instance {α} : Inhabited (Option α) where
   default := none
 
+@[macroInline] def Option.getD : Option α → α → α
+  | some x, _ => x
+  | none,   e => e
+
 inductive List (α : Type u) where
   | nil : List α
   | cons (head : α) (tail : List α) : List α
@@ -1807,6 +1811,9 @@ def SourceInfo.fromRef (ref : Syntax) : SourceInfo :=
   | some pos, some tailPos => SourceInfo.synthetic pos tailPos
   | _,        _            => SourceInfo.none
 
+def mkAtom (val : String) : Syntax :=
+  Syntax.atom SourceInfo.none val
+
 def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
   Syntax.atom src.getHeadInfo val
 
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 6692bf71b0..1c9bd6359b 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -46,8 +46,7 @@
  "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 25, "character": 13}}
-{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n\n```",
- "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n"]}
+{"rendered": "no goals", "goals": []}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 32, "character": 3}}
 {"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```",