chore(Tactic): document remaining undocumented tactics

Write documentation for the few tactics in Mathlib that have no documentation at all. After this PR and a few related ones are merged, every tactic defined in Mathlib should now have a docstring or a `@[tactic_alt]` attribute.

The documentation for `mem_tac` is pending a Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Proj.20as.20a.20scheme.3A.20.60mem_tac.60.20works.20accidentally.3F/with/563193768

Author: Vierkantor

Mathlib/Tactic/Conv.lean

@@ -18,11 +18,33 @@ public meta section
 namespace Mathlib.Tactic.Conv
 open Lean Parser.Tactic Parser.Tactic.Conv Elab.Tactic Meta
 
+/--
+`conv_lhs => cs` runs the `conv` tactic sequence `cs` on the left hand side of the target.
+
+In general, for an `n`-ary operator as the target, it traverses into the second to last argument.
+It is a synonym for `conv => arg -2; cs`.
+
+* `conv_lhs at h => cs` runs `cs` on the left hand side of hypothesis `h`.
+* `conv_lhs in pat => cs` first looks for a subexpression matching `pat` (see also the `pattern`
+  conv tactic) and then traverses into the left hand side of this subexpression.
+  This syntax also supports the `occs` clause for the pattern.
+-/
 syntax (name := convLHS) "conv_lhs" (" at " ident)? (" in " (occs)? term)? " => " convSeq : tactic
 macro_rules
   | `(tactic| conv_lhs $[at $id]? $[in $[$occs]? $pat]? => $seq) =>
     `(tactic| conv $[at $id]? $[in $[$occs]? $pat]? => lhs; ($seq:convSeq))
 
+/--
+`conv_rhs => cs` runs the `conv` tactic sequence `cs` on the right hand side of the target.
+
+In general, for an `n`-ary operator as the target, it traverses into the second to last argument.
+It is a synonym for `conv => arg -2; cs`.
+
+* `conv_lhs at h => cs` runs `cs` on the right hand side of hypothesis `h`.
+* `conv_lhs in pat => cs` first looks for a subexpression matching `pat` (see the `pattern`
+  conv tactic) and then traverses into the right hand side of this subexpression.
+  This syntax also supports the `occs` clause for the pattern.
+-/
 syntax (name := convRHS) "conv_rhs" (" at " ident)? (" in " (occs)? term)? " => " convSeq : tactic
 macro_rules
   | `(tactic| conv_rhs $[at $id]? $[in $[$occs]? $pat]? => $seq) =>

Mathlib/Tactic/GCongr/Core.lean

@@ -346,6 +346,12 @@ initialize registerBuiltinAttribute {
 
 initialize registerTraceClass `Meta.gcongr
 
+/-- `gcongr_discharger` is used by `gconger` to discharge side goals.
+
+This is an extensible tactic using [`macro_rules`](lean-manual://section/tactic-macro-extension).
+By default it calls `positivity` (after importing the `positivity` tactic).
+Example: ``macro_rules | `(tactic| gcongr_discharger) => `(tactic| positivity)``.
+-/
 syntax "gcongr_discharger" : tactic
 
 /--