[lanstin]

You want mathlib, the lean library of established results: https://github.com/leanprover-community/mathlib4

They skip steps in writing because they can generally do them and it obscures the flow of the argument to have every thing spelled out.

There is also a book on mechanics by the authors of SICP: https://mitpress.mit.edu/9780262028967/structure-and-interpr...

[lupire]

Lean doesn't have expressiveness notation. It's like Perl line noise.

[thaumasiotes]

> They skip steps in writing because they can generally do them and it obscures the flow of the argument to have every thing spelled out.

They do that in lean too; that's the idea of simp.