HTPI Lean Package
This Lean packages accompanies the online book How To Prove It with Lean. The folder HTPILib contains files with all of the definitions and theorems in the book, as well as a file defining tactics used in the book. There are also files containing all of the exercises.