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.

1. 8.1. Invoking the Simplifier
   1. 8.1.1. Parameters
2. 8.2. Rewrite Rules
3. 8.3. Simp sets
4. 8.4. Simp Normal Forms
5. 8.5. Terminal vs Non-Terminal Positions
6. 8.6. Configuring Simplification
   1. 8.6.1. Options
7. 8.7. Simplification vs Rewriting