diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index ea22016709..e7fb5b0a0d 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -369,12 +369,40 @@ private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List
   let gs ← getUnsolvedGoals
   let g ← if let `(binderIdent| $tag:ident) := tag then
     let tag := tag.getId
-    let some g ← findTag? gs tag | throwError "tag not found"
+    let some g ← findTag? gs tag | notFound gs tag
     pure g
   else
     getMainGoal
   return (g, gs.erase g)
 
+where
+  -- When the case tag is not found, construct a message that tells
+  -- the user what they could have written
+  notFound (available : List MVarId) (tag : Name) := do
+    let firstLine := m!"Case tag {showTagName tag} not found."
+    -- We must filter out the anonymous name because there may be an
+    -- anonymous goal, but users shouldn't be mistakenly encouraged
+    -- to write `case anonymous`
+    match (← available.mapM getUserName).filter (· ≠ Name.anonymous) with
+    | [] =>
+      throwError "{firstLine}\n\nThere are no cases to select."
+    | [availableName] =>
+      throwError "{firstLine}\n\nThe only available case tag is {showTagName availableName}."
+    | availableNames =>
+      throwError "Case tag {showTagName tag} not found.\n\nAvailable tags:{commaList <| availableNames.map showTagName}"
+
+  getUserName (mv : MVarId) := do return (← mv.getDecl).userName
+
+  showTagName (tagName : Name) : MessageData := m!"'{tagName}'"
+
+  -- Construct a comma-separated list that renders one per line,
+  -- indented, if it's too long
+  commaList (items : List MessageData) : MessageData :=
+    let sep := MessageData.ofFormat "," ++ Format.line
+    .group <| .nest 2 <|
+    .ofFormat .line ++ .joinSep items sep
+
+
 @[builtin_tactic «case»] def evalCase : Tactic
   | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq) =>
     for tag in tag, hs in hs do
diff --git a/tests/lean/caseSuggestions.lean b/tests/lean/caseSuggestions.lean
new file mode 100644
index 0000000000..5b212658cc
--- /dev/null
+++ b/tests/lean/caseSuggestions.lean
@@ -0,0 +1,45 @@
+/-!
+
+  # Provide case alternatives in "nonexistent tag" message
+
+  Test that the available case tags are suggested when a nonexistent
+  tag is requested. -/
+
+/-!
+  This example tests what happens when no cases are available. -/
+theorem noCases : Nat := by
+  case nonexistent =>
+    skip
+
+/-!
+  This example tests what happens when just one case is available, but
+  it wasn't picked. -/
+
+theorem oneCase : Nat := by
+  cases ()
+  case nonexistent =>
+    skip
+
+/-!
+  Check varying numbers of cases to make sure the pretty-print setup for
+  the list is correct. -/
+
+theorem twoCases : Nat := by
+  cases true
+  case nonexistent =>
+    skip
+
+theorem fourCases : Nat := by
+  cases true <;> cases true
+  case nonexistent =>
+    skip
+
+theorem eightCases : Nat := by
+  cases true <;> cases true <;> cases true
+  case nonexistent =>
+    skip
+
+theorem sixteenCases : Nat := by
+  cases true <;> cases true <;> cases true <;> cases true
+  case nonexistent =>
+    skip
diff --git a/tests/lean/caseSuggestions.lean.expected.out b/tests/lean/caseSuggestions.lean.expected.out
new file mode 100644
index 0000000000..eb7b2cb2cc
--- /dev/null
+++ b/tests/lean/caseSuggestions.lean.expected.out
@@ -0,0 +1,42 @@
+caseSuggestions.lean:11:2-12:8: error: Case tag 'nonexistent' not found.
+
+There are no cases to select.
+caseSuggestions.lean:20:2-21:8: error: Case tag 'nonexistent' not found.
+
+The only available case tag is 'unit'.
+caseSuggestions.lean:29:2-30:8: error: Case tag 'nonexistent' not found.
+
+Available tags: 'false', 'true'
+caseSuggestions.lean:34:2-35:8: error: Case tag 'nonexistent' not found.
+
+Available tags: 'false.false', 'false.true', 'true.false', 'true.true'
+caseSuggestions.lean:39:2-40:8: error: Case tag 'nonexistent' not found.
+
+Available tags:
+  'false.false.false',
+  'false.false.true',
+  'false.true.false',
+  'false.true.true',
+  'true.false.false',
+  'true.false.true',
+  'true.true.false',
+  'true.true.true'
+caseSuggestions.lean:44:2-45:8: error: Case tag 'nonexistent' not found.
+
+Available tags:
+  'false.false.false.false',
+  'false.false.false.true',
+  'false.false.true.false',
+  'false.false.true.true',
+  'false.true.false.false',
+  'false.true.false.true',
+  'false.true.true.false',
+  'false.true.true.true',
+  'true.false.false.false',
+  'true.false.false.true',
+  'true.false.true.false',
+  'true.false.true.true',
+  'true.true.false.false',
+  'true.true.false.true',
+  'true.true.true.false',
+  'true.true.true.true'