feat: explanations for cases applied to non-inductive types (#6378)

This PR adds an explanation to the error message when `cases` and
`induction` are applied to a term whose type is not an inductive type.
For `Prop`, these tactics now suggest the `by_cases` tactic. Example:
```
tactic 'cases' failed, major premise type is not an inductive type
  Prop

Explanation: the 'cases' tactic is for constructor-based reasoning as well as for applying
custom cases principles with a 'using' clause or a registered '@[cases_eliminator]' theorem.
The above type neither is an inductive type nor has a registered theorem.

Consider using the 'by_cases' tactic, which does true/false reasoning for propositions.
```

[Zulip
discussion](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Improving.20the.20error.20for.20.60cases.20p.60.20when.20.60p.60.20is.20a.20proposition/near/488882682)

src/Lean/Elab/Tactic/Induction.lean

@@ -579,12 +579,25 @@ private def checkAltsOfOptInductionAlts (optInductionAlts : Syntax) : TacticM Un
           throwErrorAt alt "more than one wildcard alternative '| _ => ...' used"
         found := true
 
-def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
+def getInductiveValFromMajor (induction : Bool) (major : Expr) : TacticM InductiveVal :=
   liftMetaMAtMain fun mvarId => do
     let majorType ← inferType major
     let majorType ← whnf majorType
     matchConstInduct majorType.getAppFn
-      (fun _ => Meta.throwTacticEx `induction mvarId m!"major premise type is not an inductive type {indentExpr majorType}")
+      (fun _ => do
+        let tacticName := if induction then `induction else `cases
+        let mut hint := m!"\n\nExplanation: the '{tacticName}' tactic is for constructor-based reasoning \
+          as well as for applying custom {tacticName} principles with a 'using' clause or a registered '@[{tacticName}_eliminator]' theorem. \
+          The above type neither is an inductive type nor has a registered theorem."
+        if majorType.isProp then
+          hint := m!"{hint}\n\n\
+            Consider using the 'by_cases' tactic, which does true/false reasoning for propositions."
+        else if majorType.isType then
+          hint := m!"{hint}\n\n\
+            Type universes are not inductive types, and type-constructor-based reasoning is not possible. \
+            This is a strong limitation. According to Lean's underlying theory, the only provable distinguishing \
+            feature of types is their cardinalities."
+        Meta.throwTacticEx tacticName mvarId m!"major premise type is not an inductive type{indentExpr majorType}{hint}")
       (fun val _ => pure val)
 
 /--
@@ -627,7 +640,7 @@ private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (inducti
         return ← getElimInfo elimName
     unless targets.size == 1 do
       throwError "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>'), and no default eliminator has been registered using attribute `[eliminator]`"
-    let indVal ← getInductiveValFromMajor targets[0]!
+    let indVal ← getInductiveValFromMajor induction targets[0]!
     if induction && indVal.all.length != 1 then
       throwError "'induction' tactic does not support mutually inductive types, the eliminator '{mkRecName indVal.name}' has multiple motives"
     if induction && indVal.isNested then

tests/lean/run/casesTactic.lean

@@ -0,0 +1,55 @@
+/-!
+# Tests of the 'cases' tactic
+-/
+
+/-!
+Error messages when not an inductive type.
+-/
+
+/--
+error: tactic 'cases' failed, major premise type is not an inductive type
+  Prop
+
+Explanation: the 'cases' tactic is for constructor-based reasoning as well as for applying custom
+cases principles with a 'using' clause or a registered '@[cases_eliminator]' theorem. The above
+type neither is an inductive type nor has a registered theorem.
+
+Consider using the 'by_cases' tactic, which does true/false reasoning for propositions.
+p : Prop
+⊢ True
+-/
+#guard_msgs in
+example (p : Prop) : True := by
+  cases p
+
+/--
+error: tactic 'cases' failed, major premise type is not an inductive type
+  Type
+
+Explanation: the 'cases' tactic is for constructor-based reasoning as well as for applying custom
+cases principles with a 'using' clause or a registered '@[cases_eliminator]' theorem. The above
+type neither is an inductive type nor has a registered theorem.
+
+Type universes are not inductive types, and type-constructor-based reasoning is not possible.
+This is a strong limitation. According to Lean's underlying theory, the only provable
+distinguishing feature of types is their cardinalities.
+α : Type
+⊢ True
+-/
+#guard_msgs in
+example (α : Type) : True := by
+  cases α
+
+/--
+error: tactic 'cases' failed, major premise type is not an inductive type
+  Bool → Bool
+
+Explanation: the 'cases' tactic is for constructor-based reasoning as well as for applying custom
+cases principles with a 'using' clause or a registered '@[cases_eliminator]' theorem. The above
+type neither is an inductive type nor has a registered theorem.
+f : Bool → Bool
+⊢ True
+-/
+#guard_msgs in
+example (f : Bool → Bool) : True := by
+  cases f