diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 4cd586b2368c..a4ff02041988 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1829,31 +1829,38 @@ structure LibrarySearchConfig where
   all : Bool := false
 
 /--
-Searches environment for definitions or theorems that can solve the goal using `exact`
-with conditions resolved by `solve_by_elim`.
-
-The optional `using` clause provides identifiers in the local context that must be
-used by `exact?` when closing the goal.  This is most useful if there are multiple
-ways to resolve the goal, and one wants to guide which lemma is used.
-
-Use `+grind` to enable `grind` as a fallback discharger for subgoals.
-Use `+try?` to enable `try?` as a fallback discharger for subgoals.
-Use `-star` to disable fallback to star-indexed lemmas (like `Empty.elim`, `And.left`).
-Use `+all` to collect all successful lemmas instead of stopping at the first.
+`exact?` searches the environment for definitions or theorems that solve the goal using `exact`,
+with all side conditions resolved by `solve_by_elim`. After printing the suggestions,
+`exact?` closes the current goal with `sorry`. `exact?` is a proof writing tool that should not be
+left in finished code.
+
+* `exact? using h₁, ... hₙ` requires that the local hypotheses `h₁`, ..., `hₙ` are
+  used by `exact?` when closing the goal.  This is most useful if there are multiple
+  ways to resolve the goal, and one wants to guide which lemma is used.
+* `exact? (config := cfg)` specifies the configuration using `cfg : LibrarySearchConfig`.
+  In particular:
+  * `exact? +grind` enables `grind` as a fallback discharger for subgoals.
+  * `exact? +try?` enables `try?` as a fallback discharger for subgoals.
+  * `exact? -star` disables fallback to star-indexed lemmas (like `Empty.elim`, `And.left`).
+  * `exact? +all` collects all successful lemmas instead of stopping at the first.
 -/
 syntax (name := exact?) "exact?" optConfig (" using " (colGt ident),+)? : tactic
 
 /--
-Searches environment for definitions or theorems that can refine the goal using `apply`
-with conditions resolved when possible with `solve_by_elim`.
-
-The optional `using` clause provides identifiers in the local context that must be
-used when closing the goal.
+`apply?` searches the environment for definitions or theorems that solve the goal using `apply`,
+possibly with side conditions resolved by `solve_by_elim`. After printing the suggestions,
+`apply?` closes the current goal with `sorry`. `apply?` should not be left in finished code;
+it is a search tool.
 
-Use `+grind` to enable `grind` as a fallback discharger for subgoals.
-Use `+try?` to enable `try?` as a fallback discharger for subgoals.
-Use `-star` to disable fallback to star-indexed lemmas.
-Use `+all` to collect all successful lemmas instead of stopping at the first.
+* `apply? using h₁, ... hₙ` requires that the local hypotheses `h₁`, ..., `hₙ` are
+  used by `apply?` when closing the goal.  This is most useful if there are multiple
+  ways to resolve the goal, and one wants to guide which lemma is used.
+* `apply? (config := cfg)` specifies the configuration using `cfg : LibrarySearchConfig`.
+  In particular:
+  * `apply? +grind` enables `grind` as a fallback discharger for subgoals.
+  * `apply? +try?` enables `try?` as a fallback discharger for subgoals.
+  * `apply? -star` disables fallback to star-indexed lemmas (like `Empty.elim`, `And.left`).
+  * `apply? +all` collects all successful lemmas instead of stopping at the first.
 -/
 syntax (name := apply?) "apply?" optConfig (" using " (colGt term),+)? : tactic
 
@@ -1863,13 +1870,12 @@ Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.
 syntax rewrites_forbidden := " [" (("-" ident),*,?) "]"
 
 /--
-`rw?` tries to find a lemma which can rewrite the goal.
-
-`rw?` should not be left in proofs; it is a search tool, like `apply?`.
-
-Suggestions are printed as `rw [h]` or `rw [← h]`.
+`rw?` searches the environment for lemmas which can rewrite the goal. After printing the suggestions,
+`rw?` applies the first, most specific result. Suggestions are printed as `rw [h]` or `rw [← h]`.
+`rw?` should not be left in finished code; it is a search tool.
 
-You can use `rw? [-my_lemma, -my_theorem]` to prevent `rw?` using the named lemmas.
+* `rw? at loc` tries to rewrite at location(s) `loc`.
+* `rw? [-my_lemma, -my_theorem]` prevents `rw?` from using the named lemmas as suggestions.
 -/
 syntax (name := rewrites?) "rw?" (ppSpace location)? (rewrites_forbidden)? : tactic
 
@@ -1889,8 +1895,8 @@ macro (name := showTermElab) tk:"show_term " t:term : term =>
   `(term| no_implicit_lambda% (show_term_elab%$tk $t))
 
 /--
-The command `by?` will print a suggestion for replacing the proof block with a proof term
-using `show_term`.
+`by? tacs` runs the tactic sequence `tacs` and suggests to replace the `by?` block with the proof
+term generated by the tactics.
 -/
 macro (name := by?) tk:"by?" t:tacticSeq : term => `(show_term%$tk by%$tk $t)