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

You want mathlib, the lean library of established results: https://github.com/leanprover-community/mathlib4 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-interpretation-of-classical-mechanics/ https://mitpress.mit.edu/9780262028967/structure-and-interpr...