chore(Tactic/CasesM): improve casesm, cases_type and constructorm tactic docstrings (leanprover-community#34538)

This PR (re)writes the docstrings for the `casesm`, `cases_type` and `constructorm` tactics to consistently match the official style guide, to make sure they are complete while not getting too long.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

Author: Vierkantor

Mathlib/Tactic/CasesM.lean

@@ -91,17 +91,26 @@ def elabCasesM (pats : Array Term) (recursive allowSplit : Bool) : TacticM Unit
   liftMetaTactic (casesMatching (matchPatterns pats) recursive allowSplit)
 
 /--
-* `casesm p` applies the `cases` tactic to a hypothesis `h : type`
-  if `type` matches the pattern `p`.
-* `casesm p_1, ..., p_n` applies the `cases` tactic to a hypothesis `h : type`
-  if `type` matches one of the given patterns.
-* `casesm* p` is a more efficient and compact version of `· repeat casesm p`.
+`casesm p` searches for the first hypothesis `h : type` where `type` matches the term `p`,
+and splits the main goal by cases on `h`. Use holes in `p` to indicate arbitrary subexpressions,
+for example `casesm _ ∧ _` will match any conjunction. `casesm p` fails if no hypothesis type
+matches `p`.
+
+* `casesm p_1, ..., p_n` searches for a hypothesis `h : type` where `type` matches one or more of
+  the given patterns `p_1`, ... `p_n`, and splits the main goal by cases on `h`.
+* `casesm* p` repeatedly performs case splits until no more hypothesis type matches `p`.
+  This is a more efficient and compact version of `· repeat casesm p`.
   It is more efficient because the pattern is compiled once.
-* `casesm! p` only applies `cases` if the number of resulting subgoals is <= 1.
+* `casesm! p` and `casesm!* p` skip a hypothesis if the main goal would be replaced with two or more
+  subgoals.
 
-Example: The following tactic destructs all conjunctions and disjunctions in the current context.
+Example:
 ```
-casesm* _ ∨ _, _ ∧ _
+example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
+  -- The following tactic destructs all conjunctions and disjunctions in the current context.
+  casesm* _∨_, _∧_
+  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
+  · clear ‹c› ‹d› ‹e› ‹f›; trivial
 ```
 -/
 elab (name := casesM) "casesm" recursive:"*"? ppSpace pats:term,+ : tactic => do
@@ -118,15 +127,24 @@ def elabCasesType (heads : Array Ident)
   liftMetaTactic (casesType heads recursive allowSplit)
 
 /--
-* `cases_type I` applies the `cases` tactic to a hypothesis `h : (I ...)`
-* `cases_type I_1 ... I_n` applies the `cases` tactic to a hypothesis
-  `h : (I_1 ...)` or ... or `h : (I_n ...)`
-* `cases_type* I` is shorthand for `· repeat cases_type I`
-* `cases_type! I` only applies `cases` if the number of resulting subgoals is <= 1.
-
-Example: The following tactic destructs all conjunctions and disjunctions in the current goal.
+`cases_type I` searches for a hypothesis `h : type` where `I` has the form `(I ...)`, and splits the
+main goal by cases on `h`. `cases_type p` fails if no hypothesis type has the identifier `I` as its
+head symbol.
+
+* `cases_type I_1 ... I_n` searches for a hypothesis `h : type` where `type` has one or more of
+  `I_1`, ..., `I_n` as its head symbol, and splits the main goal by cases on `h`.
+* `cases_type* I` repeatedly performs case splits until no more hypothesis type has `I` as its head
+  symbol. This shorthand for `· repeat cases_type I`.
+* `cases_type! p` and `cases_type!* p` skip a hypothesis if the main goal would be replaced with two
+  or more subgoals.
+
+Example:
 ```
-cases_type* Or And
+example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
+  -- The following tactic destructs all conjunctions and disjunctions in the current context.
+  cases_type* Or And
+  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
+  · clear ‹c› ‹d› ‹e› ‹f›; trivial
 ```
 -/
 elab (name := casesType) "cases_type" recursive:"*"? heads:(ppSpace colGt ident)+ : tactic =>
@@ -167,15 +185,18 @@ where
       return (acc.push g)
 
 /--
-* `constructorm p_1, ..., p_n` applies the `constructor` tactic to the main goal
-  if `type` matches one of the given patterns.
-* `constructorm* p` is a more efficient and compact version of `· repeat constructorm p`.
-  It is more efficient because the pattern is compiled once.
+`constructorm p_1, ..., p_n`, where the main goal has type `type`, applies the first matching
+constructor for `type`, if `type` matches one of the given patterns. If `type` does not match any
+of the patterns, `constructorm` fails.
+
+* `constructorm* p_1, ..., p_n` repeatedly applies a constructor until the goal no longer matches
+  `p_1`, ..., `p_n`. This is a more efficient and compact version of
+  `· repeat constructorm p_1, ..., p_n`. It is more efficient because the pattern is compiled once.
 
-Example: The following tactic proves any theorem like `True ∧ (True ∨ True)` consisting of
-and/or/true:
+Examples:
 ```
-constructorm* _ ∨ _, _ ∧ _, True
+example : True ∧ (True ∨ True) := by
+  constructorm* _ ∨ _, _ ∧ _, True
 ```
 -/
 elab (name := constructorM) "constructorm" recursive:"*"? ppSpace pats:term,+ : tactic => do