 mathlib4

Here is a specific minimal example of how to use mathlib4: proofassistants.stackexchange.com/questions/2526/how-to-run-lean4-with-mathlib-manually/5299#5299