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