8. The Simplifier
The simplifier is one of the most-used features of Lean. It performs inside-out rewriting of terms based on a database of simplification rules. The simplifier is highly configurable, and a number of tactics use it in different ways.