How To Prove It with Lean
= 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.