feat: list the valid case tags when the user writes an invalid one

Before, Lean would simply emit the message "tag not found". With this
change, it also tells the user what they could have written that would
be accepted.

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

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

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'