# Tactics | Tactic Name | Ex. Expr. | What does it do? | | ----------- | --------- | ----------------------------------------- | | `rfl` | $X = X$ | Proves all theorems of the observed form. | | `rw` | | |