diff --git a/src/Init/Grind/Attr.lean b/src/Init/Grind/Attr.lean
index f7b0b33d9d..589ec450a8 100644
--- a/src/Init/Grind/Attr.lean
+++ b/src/Init/Grind/Attr.lean
@@ -135,7 +135,7 @@ Each time it encounters a subexpression which covers an argument which was not
 previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
 If `grind!` is used, then only minimal indexable subexpressions are considered.
 -/
-syntax grindDef    := "." (grindGen)?
+syntax grindDef    := patternIgnore("." <|> "·") (grindGen)?
 /--
 The `usr` modifier indicates that this theorem was applied using a
 **user-defined instantiation pattern**. Such patterns are declared with
@@ -215,9 +215,47 @@ syntax grindMod :=
     <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
     <|> grindCases <|> grindIntro <|> grindExt <|> grindGen <|> grindSym <|> grindInj
     <|> grindDef
+
+/--
+Marks a theorem or definition for use by the `grind` tactic.
+
+An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
+controls how `grind` uses the declaration:
+* whether it is applied forwards, backwards, or both,
+* whether equalities are used on the left, right, or both sides,
+* whether case-splits, constructors, extensionality, or injectivity are applied,
+* or whether custom instantiation patterns are used.
+
+See the individual modifier docstrings for details.
+-/
 syntax (name := grind) "grind" (ppSpace grindMod)? : attr
+/--
+Like `@[grind]`, but enforces the **minimal indexable subexpression condition**:
+when several subterms cover the same free variables, `grind!` chooses the smallest one.
+
+This influences E-matching pattern selection.
+
+### Example
+```lean
+theorem fg_eq (h : x > 0) : f (g x) = x
+
+@[grind <-] theorem fg_eq (h : x > 0) : f (g x) = x
+-- Pattern selected: `f (g x)`
+
+-- With minimal subexpression:
+@[grind! <-] theorem fg_eq (h : x > 0) : f (g x) = x
+-- Pattern selected: `g x`
+-/
 syntax (name := grind!) "grind!" (ppSpace grindMod)? : attr
+/--
+Like `@[grind]`, but also prints the pattern(s) selected by `grind`
+as info messages. Useful for debugging annotations and modifiers.
+-/
 syntax (name := grind?) "grind?" (ppSpace grindMod)? : attr
+/--
+Like `@[grind!]`, but also prints the pattern(s) selected by `grind`
+as info messages. Combines minimal subexpression selection with debugging output.
+-/
 syntax (name := grind!?) "grind!?" (ppSpace grindMod)? : attr
 end Attr
 end Lean.Parser
diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index 5d52ab3912..d45a9b9a84 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Attr
 public import Init.Core
-
 public section
 
 namespace Lean.Grind
@@ -98,8 +96,16 @@ structure Config where
   zeta := true
   /--
   When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
+  This solver also support commutative semirings, fields, and normalizer non-commutative rings and
+  semirings.
   -/
   ring := true
+  /--
+  Maximum number of steps performed by the `ring` solver.
+  A step is counted whenever one polynomial is used to simplify another.
+  For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
+  used to simplify the second to `-1 * y^3 + x * y`.
+  -/
   ringSteps := 10000
   /--
   When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
@@ -114,6 +120,12 @@ structure Config where
   When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
   -/
   ac := true
+  /--
+  Maximum number of steps performed by the `ac` solver.
+  A step is counted whenever one AC equation is used to simplify another.
+  For example, given `ma x z = w` and `max x (max y z) = x`, the first can be
+  used to simplify the second to `max w y = x`.
+  -/
   acSteps := 1000
   /--
   Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
@@ -125,7 +137,11 @@ structure Config where
   -/
   abstractProof := true
   /--
-  When `true` (default: `true`), uses procedure for handling injective functions.
+  When `true` (default: `true`), enables the procedure for handling injective functions.
+  In this mode, `grind` takes into account theorems such as:
+  ```
+  @[grind inj] theorem double_inj : Function.Injective double
+  ```
   -/
   inj := true
   deriving Inhabited, BEq