diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 7e018bddb5..4b7988b74c 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -214,7 +214,7 @@ syntax (name := apply) "apply " term : tactic
 syntax (name := exact) "exact " term : tactic
 syntax (name := refine) "refine " term : tactic
 syntax (name := refine') "refine' " term : tactic
-syntax (name := case) "case " ident " => " tacticSeq : tactic
+syntax (name := case) "case " ident (ident <|> "_")* " => " tacticSeq : tactic
 syntax (name := allGoals) "allGoals " tacticSeq : tactic
 syntax (name := focus) "focus " tacticSeq : tactic
 syntax (name := skip) "skip" : tactic
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 4da4516018..e89f924dc7 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -541,7 +541,7 @@ def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α :
   withRef (mkNullNode #[arrow, body]) x
 
 @[builtinTactic «case»] def evalCase : Tactic
-  | `(tactic| case $tag =>%$arr $tac:tacticSeq) => do
+  | `(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do
     let tag := tag.getId
     let gs ← getUnsolvedGoals
     let some g ← findTag? gs tag | throwError "tag not found"