§ 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 simpfirst 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.