Mathematics Resources for learning Lean (4) Lean 4 manual Lean 4 reference Theorem proving in Lean 4 Functional programming in Lean 4 Lean VSCode abbreviations/snippets About Proofs can definitely be shorter and clearer. (feel free to PR)