Part A: the mathematics
The material in this course is divided into sections, each of which corresponds to a mathematical topic. For each section there is some Lean code in the course’s github repository. For some of the earlier sections (which should probably be done in order) there are some hints and notes here in the course notes.
Note that, in contrast, the material in parts B and C of these notes can be read in any order.