HepLean Documentation

Mathlib.Tactic.Common

This file imports all tactics which do not have significant theory imports, and hence can be imported very low in the theory import hierarchy, thereby making tactics widely available without needing specific imports.

We include some commented out imports here, with an explanation of their theory requirements, to save some time for anyone wondering why they are not here.

We also import theory-free linters, commands, and utilities which are useful to have low in the import hierarchy.

Register tactics with hint. #