https://lean-lang.org/theorem_proving_in_lean4/title_page.ht...
You may need to use them in tandem, but I have found it much more productive to jump to the “number theory” section of TFA then to step through the official resource.
This resource also has its code online: https://github.com/hrmacbeth/math2001/tree/main/Math2001
One major ommission from TFA is lean's built in package manager and package builder lake: https://lean-lang.org/lean4/doc/setup.html#lake