# Tactics
| Tactic Name | Ex. Expr.    | What does it do?                                              |
| ----------- | ------------ | ------------------------------------------------------------- |
| `rfl`       | $X = X$      | Proves all theorems of the observed form.                     |
| `rw [h]`    | $Y = X+a$    | 'Rewrite' an equation using an assumption 'h' or similar.     |
| `succ x`    | $Y = Y+1$    | 'Successor' says that some number is bigger than another one. |
| `\l`        | $\leftarrow$ | Does the opposite of rw. Turns Ys into Xs                     |
| `repeat`    | n/a          | Repeats the following action                                  |