chore: update grind docstring (#11654)

This PR updates the `grind` docstring. It was still mentioning `cutsat`
which has been renamed to `lia`. This issue was reported during ItaLean.

src/Init/Grind/Tactics.lean

@@ -156,10 +156,10 @@ theorems and helps prevent an excessive number of instantiations.
 - `grind only [<name>, ...]` is like `grind [<name>, ...]` but does not use theorems tagged with `@[grind]`.
 - `grind (gen := <num>)` sets the maximum generation.
 
-### Linear integer arithmetic (`cutsat`)
+### Linear integer arithmetic (`lia`)
 
 `grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an
-integrated decision procedure called **`cutsat`**.  It understands
+integrated decision procedure called **`lia`**.  It understands
 
 * equalities   `p = 0`
 * inequalities  `p ≤ 0`
@@ -172,7 +172,7 @@ This *model-based* search is **complete for LIA**.
 
 #### Key options:
 
-* `grind -cutsat` disable the solver (useful for debugging)
+* `grind -lia` disable the solver (useful for debugging)
 * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ)
 
 #### Examples:
@@ -297,7 +297,7 @@ syntax (name := grindTrace)
 /--
 `cutsat` solves linear integer arithmetic goals.
 
-It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `cutsat` solver.
+It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `lia` solver.
 Please use `grind` instead if you need additional capabilities.
 
 **Deprecated**: Use `lia` instead.
@@ -307,7 +307,7 @@ syntax (name := cutsat) "cutsat" optConfig : tactic
 /--
 `lia` solves linear integer arithmetic goals.
 
-It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `cutsat` solver.
+It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `lia` solver.
 Please use `grind` instead if you need additional capabilities.
 -/
 syntax (name := lia) "lia" optConfig : tactic