feat: explanations for cases applied to non-inductive types

[kmill]

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

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fc4305ab15d7137f6bda64a557dc2ca9c6fc460f --onto 48be424eaa2ae06972e9cfec4d355906b532204d. (2024-12-13 17:14:52)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 58ffd15a8f4816473bda4c7b9b41e6c4eb2e00f1 --onto 48be424eaa2ae06972e9cfec4d355906b532204d. (2024-12-13 19:03:35)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 58ffd15a8f4816473bda4c7b9b41e6c4eb2e00f1 --onto a8a160b09147c3225150703ac727eea6ee9a3b0e. (2024-12-16 22:15:22)