Core tactic documentation #

This file adds the majority of the interactive tactics from core Lean (i.e. pre-mathlib) to the API documentation.

TODO #

• Make a PR to core changing core docstrings to the docstrings below, and also changing the docstrings of cc, simp and conv to the ones already in the API docs.

• SMT tactics are currently not documented.

• rsimp and constructor_matching are currently not documented.

• dsimp deserves better documentation.