1. Install Lean 4 and VS Code following these instructions.
2. Make sure you have git installed.
3. Let's say you want to use the copilot lean project.
4. cd copilot.
5. lake exe cache get.
6. Use VS Code to open the copilot folder (not its subfolder or parent foler).

At that point, you can open the textbook in a side panel in VS Code as follows:

1. Type ctrl-shift-P (command-shift-P in macOS).
2. Type Lean 4: Docview: Open Docview in the bar that appears, and then press return. (You can press return to select it as soon as it is highlighted in the menu.)

https://codespaces.new as in https://github.com/leanprover-community/mathematics_in_lean/blob/master/README.md

1. https://github.com/leanprover-community/mathematics_in_lean/blob/master/README.md