Part C: Tactics
Here is some documentation for the tactics which we will be using in the course. Note also that the Lean community website has extensive documentation on all the tactics in Lean and mathlib. Check out the tactic page on the community website here if you want to explore beyond the tactics below, or see another take on what they do.