Lean-4-Literature

Beginner friendly

Theorem Proving in Lean 4 - Use Lean 4 as a proof assistant to prove theorems.
Functional Programming in Lean - Use Lean 4 as a programming language.
Mathematics in Lean - Use Lean 4 to do 'common' mathematics.
The Mechanics of Proof - Use Lean 4 to do 'common' mathematics.
The Hitchhiker's Guide to Logical Verification - Use Lean 4 to do 'common' computer science.
Logic and Proof - Use Lean 4 to do logic in Lean 4.

Intermediate and onwards

Metaprogramming in Lean 4 - Extend Lean 4 with custom functionality.
Type Checking in Lean 4 - Learn about Lean 4 metatheory.
Scientific Computing in Lean - WIP - Modern approach to scientific computing melding convenience of use, correctness, ~~and performance~~.
The Lean Language Reference - The language reference.

This list is a superset of documentation recommended at the official Lean 4 website.

Lean-4-not-so-Literature

WARNING: subjective and broad; grain of salt recommended, reader discretion required.

List of thoughts/guidelines. While I may use examples to explain what to do / not to do - I do not say why for the sake of brevity. Why left as an exercise for the reader. While I am happy to discuss nuances and pertinence of these at length, this is not a repo in which to do it.

Environment

Use VS Code and its Lean 4 extension.
Use JuliaMono font.

Lean

Do not (ab)use dependent types. Give strong preference to extrinsic properties.

section Bad
def foo (n : Nat) : { m : Nat // 42 < m } := ...
end Bad

section Good
def foo (n : Nat) : Nat := ...
theorem 42_lt_foo {n : Nat) : 42 < foo n := ...
end Good

Do not unfold more than 1 definition per theorem. State lemmas about definitions you use, unfold these definitions in the lemmas that are specifically about them.
Only use simp [...] (and its derivatives, a'la aesop) to discharge the enclosing goal - i.e. as the final tactic in a goal. Use simp only otherwise. Invoking simp? gives you the appropriate simp only to use, if you 'must' use simp in the middle of a proof.