Lean Documentation
Although the course texts are intended to be self contained, the main Lean page includes documentation, a community forum (Zulip), and pointers to many other useful resources.
Two free online books are especially useful companions for this course: Theorem Proving in Lean 4, which covers the core language and how to state and prove theorems, and Functional Programming in Lean, which covers Lean as a general-purpose functional programming language. If you go on to use Lean's math library, Mathematics in Lean is the standard introduction to mathlib.
Lean Development Environments
We recommend using VS Code with the official Lean 4 extension, which gives you an interactive display of the proof state as you edit. Lean toolchains and projects are managed with elan (analogous to rustup for Rust), which the extension will prompt you to install if it is not already on your system.
See the Preface of the course textbook for instructions for downloading and installation, and for setting up the course's Lean project so that the exercises typecheck against the right toolchain and dependencies.
Please post on the course discussion site if you encounter difficulties setting up your Lean development environment.