diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index b80df98467..d47444d4ec 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -469,7 +469,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
 private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List MVarId) := do
   let gs ← getUnsolvedGoals
   let g ← if let `(binderIdent| $tag:ident) := tag then
-    let tag := tag.getId
+    let tag := tag.getId.eraseMacroScopes
     let some g ← findTag? gs tag | notFound gs tag
     pure g
   else
diff --git a/tests/lean/run/caseTacInMacros.lean b/tests/lean/run/caseTacInMacros.lean
new file mode 100644
index 0000000000..2743033e43
--- /dev/null
+++ b/tests/lean/run/caseTacInMacros.lean
@@ -0,0 +1,22 @@
+def f (n : Nat) := n + 1
+
+macro "mymacro1 " h:ident : tactic =>
+  `(tactic| {
+      cases $h:ident with
+      | zero => decide
+      | succ => simp_arith [f]
+  })
+
+example : f n > 0 := by
+  mymacro1 n -- works
+
+macro "mymacro2 " h:ident : tactic =>
+  `(tactic| {
+      cases $h:ident
+      case zero => decide
+      case succ => simp_arith [f]
+  })
+
+example : f n > 0 := by
+  -- Should **not** generate: Case tag 'zero._@.cases3._hyg.747' not found.
+  mymacro2 n