How To Prove It with Lean
ID: how-to-prove-it-with-lean
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.
New to topics? Read the docs here!