diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 542d0c1e83..10da50fc31 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -279,6 +279,10 @@ syntax (name := constructor) "constructor" : tactic
 `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`, or else fails.
 `case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. -/
 syntax (name := case) "case " (ident <|> "_") (ident <|> "_")* " => " tacticSeq : tactic
+/--
+`next => tac` focuses on the next goal solves it using `tac`, or else fails.
+`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. -/
+macro "next " args:(ident <|> "_")* " => " tac:tacticSeq : tactic => `(tactic| case _ $(args.getArgs)* => $tac)
 
 /-- `allGoals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "allGoals " tacticSeq : tactic
diff --git a/tests/lean/run/matchEqs.lean b/tests/lean/run/matchEqs.lean
index 872fc9a3b8..e7f5a07904 100644
--- a/tests/lean/run/matchEqs.lean
+++ b/tests/lean/run/matchEqs.lean
@@ -21,9 +21,9 @@ test% f.match_1
 theorem ex (x : List Nat) : f x > 0 := by
   simp [f]
   induction x using f.match_1.splitter
-  case _ => simp [f.match_1.eq_1]
-  case _ => simp [f.match_1.eq_2]
-  case _ x h1 h2 =>
+  next => simp [f.match_1.eq_1]
+  next x => simp [f.match_1.eq_2]
+  next x h1 h2 =>
     rw [f.match_1.eq_3]
     . decide
     . exact h1