This article is motivated by my experiences learning lean, as I learn I'll document useful things that helped me get to where I am today.

- theorem proving in lean: good way to understand lean in more depth without getting into the implementation.
- list and description of all tactics at a high level
- lean FAQ

- natural number game: good introduction to lean
- tutorial from leanprover-community
- formalising mathematics 2021
- formalising mathematics 2022

Since there are already prebuilt tools for vscode that's what I started using. The lean extension is here, I pair it with the neovim extensions as well.

Additionally there are many shortcuts which allow you to write useful notation, see the following table:

- logic
**∨**: shortcut (\or) meaning: or**∧**: shortcut (\and) meaning: and**→**: shortcut (\r) meaning: of (with order reversed and sometimes only the conclusion is stated)**↔**: shortcut (\iff) meaning: iff (sometimes omitted along with the right hand side of the iff)**¬**: shortcut (\n) meaning: not**∃**: shortcut (\ex) meaning: exists / bex (bounded exists)**∀**: shortcut (\fo) meaning: all / forall / ball (bounded forall)**=**: shortcut eq (often omitted)**≠**: shortcut (\ne) meaning: ne**∘**: shortcut (\o) meaning: comp- set
**∈**: shortcut (\in) meaning mem**∪**: shortcut (\cup) meaning union**∩**: shortcut (\cap) meaning inter**⋃**: shortcut (\bigcup) meaning Union / bUnion**⋂**: shortcut (\bigcap) meaning Inter / bInter**\**: shortcut (\\) meaning sdiff**ᶜ**: shortcut (\^c) meaning compl- algebra
**0**: meaning zero**+**: meaning add**-**: meaning neg (unary) / sub (binary)**1**: meaning one*****: meaning mul**^**: meaning pow**/**: meaning div**•**: shortcut (\bu) meaning smul**⁻**:¹shortcut (\-1) meaning inv**∣**: shortcut (\|) meaning dvd- lattices
**<**: meaning lt**≤**: shortcut (\le) meaning le**⊔**: shortcut (\sqcup) meaning sup**⊓**: shortcut (\sqcap) meaning inf**⨆**: shortcut (\Sqcup) meaning Sup**⨅**: shortcut (\Sqcap) meaning Inf (edited)

Remember that the order of operations is ¬, ∧, ∨, (↔, →)

**nat**- natural numbers**fun**- function**int**- integers**rat**- rationals**zmod**- integers mod n**fp**- floating-point numbers**eq**- equals

If you are looking for an elementary result, start your search in **data**,

- data.nat.modeq - congruences modulo a natural number
- data.zmod.basic - integers mod n
- fermats little theorem

- analysis.special_functions.logb - real logarithm base b