How To Prove It with Lean (source code)

= How To Prove It with Lean 

https://djvelleman.github.io/HTPIwL

This tutorial has the merit of actually trying you to do some meaningful mathematics before teaching you a billion items of syntax and dependent type theory nuances.