Lean 4 survival guide for Lean 3 users

Links

• Lean 4 cheatsheet: https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf
• Differences with Lean 3 from the official Lean 4 manual: https://leanprover.github.io/lean4/doc/lean3changes.html

Syntax changes

• Function notation changed from λ x, f x to fun x => f x or λ x => f x. If you import (almost) any file from mathlib, you can also use fun x ↦ f x or λ x ↦ f x.
• For infix notation like + you cannot use (+) or (+ n) anymore, instead use (· + ·) or (· + n). The · (entered with \.) is an anonymous lambda expression. The lambda expression will be inserted at the nearest enclosing parentheses (see linked manual page).

Naming Conventions

Tactic changes

Tactic block changes

• Enter tactic mode by using by and then a newline, and indenting the tactics. Example:

example : True := by
  trivial

• Don't place comma's after tactics, you can go to the next tactic if you write it on a new line (in the same column)
• If you have multiple goals, you can focus on the first goal using \.

example : (True → p) → q → p ∧ q := by
  intros hp hq
  constructor
  · apply hp
    trivial
  · exact hq

• If you want multiple tactics on the same line, you can use tac1; tac2 (which corresponds to tac1, tac2 in Lean 3) or tac1 <;> tac2 (which corresponds to tac1; tac2 in Lean 3)

Specific tactic changes

• The analogue of refine is refine'.
• The square brackets in rw [h] are mandatory
• split has been removed. Use constructor.
• To work on the first goal use · exact foo instead of {exact foo}. Note that · is \., not \cdot.

New features

• Named implicit arguments, like f (x := 3)

How do I do X?