To the author, Lean is not mathlib (A fact that you will probably get sick of hearing if you spend time in the zulip). If your objective with lean is to use mat

To the author, Lean is not mathlib (A fact that you will probably get sick of hearing if you spend time in the zulip). If your objective with lean is to use mathlib, you should try following the mathlib tutorial as well.