Tactic doc cleanup about mathlib HOT 6 CLOSED

I know documentation for convert is missing as well.

from mathlib.

It would be nice to clean this before the Amsterdam meeting. Maybe I'll have time for it next week, but don't hesitate to tackle it.

from mathlib.

I noticed while reviewing #757 that norm_num is missing its own section in the tactic docs.

Right now it's just mentioned as something you can do inside conv.

from mathlib.

swap also seems to be missing.

from mathlib.

swap is now documented: #1272

from mathlib.

Tactics that are missing as of today: (please check boxes and add tactics if things change)

• abel
• apply' + variants
  * [ ] auto_cases (this isn't interactive)
• generalize_proofs
• norm_num
• variants of nth_rewrite (in the rewrite_all folder)
• ring2?
• scc
• slice
• split_ifs
• subtype_instance
• tauto
• wlog

Also:

* [ ] Sort tactics by name (obsolete with the new doc view)

Maybe also the following non-interactive tactics should be mentioned?

• chain
• run_once (and other tactics in local_cache?)
• transfer
• transform_decl_with_prefix_* (formerly named transport)

Do we want a separate file with non-tactic things in the tactic folder? #1815 added a new commands doc file; is that sufficient or do we want to break things up further?

• ancestor attribute
• alias
• doc_blame (in commands doc)
• explode (in commands doc)
• find (in commands doc)
• localized/open_locale (in commands doc)
• mk_iff_of_inductive_prop
• reassoc (is in tactic doc), reassoc_axiom is in commands doc
• def_replacer (is in tactic doc)
• sanity_check lint (in commands doc)
• where (in commands doc)

from mathlib.