ยง Big list of lean tactics

conv => ...
: rewrite in pattern. example: conv in x + 1 => rw ...

split
allows one to deal with the cases of a match pattern. This also allows one to case on an if
condition. 
cases H: inductive with  cons1 => sorry  cons2 => sorry
is used to perform case analysis on an inductive type. 
cases H; case cons1 => { ... }; case cons2 => { ... }
is the same , but with slightly different syntax. 
rewrite [rule] (at H)?
performs the rewrite with rule. But generally, prefer simp [rule] (at H)
, because simp
first runs the rewrite, and then performs reduction. But if simp
does not manage to perform a rewrite, it does not perform reduction, which can lead to weird cases like starting with let H = x = true in match x  true => 1, false => 2
. On running rewrite [H]
, we get match true  true => 1, false => 2
. And now if we run simp
, it performs no reduction. On the other hand, if we had run simp [H]
, it would rewrite to match true  true => 1  false => 2
and then also perform reduction to give 1
.