Using mathlib4 as a dependency
In a new project
In an existing project
Getting started
Updating mathlib4
In VS Code
From the command line
Dealing with breakages from updating
On lake exe cache