lean-quick-reference

name	lean-quick-reference
description	Consolidated cheatsheets for Lean 4 syntax, tactics, type classes, monads, and common patterns. Use for quick lookup or when you need a reminder.
allowed-tools	Read, Grep, Glob

Lean 4 Quick Reference

Consolidated cheatsheets for Lean 4 syntax, tactics, type classes, and common patterns. Use for quick lookup of syntax or when you need a reminder.

Trigger terms: "lean syntax", "cheatsheet", "quick reference", "lean help", "how to lean"

---

Type Definition Syntax

-- Structure (product type)
structure Point where
  x : Float
  y : Float
  deriving Repr

-- Inductive (sum type)
inductive Option (α : Type) where
  | none : Option α
  | some : α → Option α

-- Type alias
abbrev Nat2 := Nat × Nat

---

Function Definition

-- Basic
def add (x y : Nat) : Nat := x + y

-- Pattern matching
def isZero : Nat → Bool
  | 0 => true
  | _ => false

-- Where clause
def f (x : Nat) : Nat := helper x
where helper n := n + 1

-- Lambda
fun x => x + 1
λ x => x + 1

---

Type Class Quick Reference

Class	Provides	Infix
Add	add	+
Mul	mul	*
BEq	beq	==
Ord	compare	<, ≤
ToString	toString	-
Repr	repr	-
Functor	map	<$>
Applicative	pure, seq	<*>
Monad	pure, bind	>>=
Alternative	failure, orElse	`<

---

Monad Cheatsheet

Monad	Purpose	Create	Fail
Option	Maybe value	some x	none
Except ε	Error handling	Except.ok x	Except.error e
State σ	Mutable state	pure x	-
Reader ρ	Environment	pure x	-
IO	Side effects	pure x	throw

do-notation:

do let x ← action1    -- bind
   let y := expr       -- let
   action2             -- sequence
   pure result         -- return

---

Tactic Cheatsheet

Tactic	Purpose	Example
rfl	Reflexive equality	example : 1 = 1 := by rfl
exact	Provide proof term	exact hp
apply	Apply lemma	apply And.intro
intro	Introduce hypothesis	intro hp
constructor	Apply constructor	Splits ∧ goals
left/right	Choose ∨ branch	left; exact hp
cases	Case analysis	cases h
induction	Induction	induction n
rw	Rewrite	rw [h]
simp	Simplify	simp [lemmas]
decide	Decidable props	by decide
omega	Linear arithmetic	by omega
trivial	Prove True	trivial
contradiction	From contradictions	contradiction
have	Introduce fact	have h : T := proof
show	Clarify goal	show T

---

Logical Connectives

Connective	Type	Intro	Elim
→	Function	fun hp => ...	f hp
∧	And	⟨hp, hq⟩	h.left, h.right
∨	Or	Or.inl hp	cases h
¬	Not	fun hp => ...	absurd hp hnp
∀	Pi	fun x => ...	h x
∃	Exists	⟨w, hw⟩	obtain ⟨w, hw⟩ := h
↔	Iff	⟨mp, mpr⟩	h.mp, h.mpr

---

Commands

Command	Purpose
#check expr	Show type
#eval expr	Evaluate
#print name	Show definition
#reduce expr	Reduce to normal form
example : T := proof	Anonymous theorem
theorem name : T := proof	Named theorem
def name : T := expr	Definition

---

Common Patterns

Safe indexing:

arr.get ⟨i, by decide⟩  -- Fin for bounds proof
arr[i]?                  -- Option result
arr[i]!                  -- Panic if invalid

Pattern matching:

match x with
| pattern1 => result1
| pattern2 => result2

If-then-else with hypothesis:

if h : condition then
  -- h : condition available here
else
  -- h : ¬condition available here

---

File Structure

import Lean           -- Import module
namespace MySpace     -- Open namespace
section MySection     -- Scoped section
variable (x : Nat)    -- Implicit parameter
open OtherSpace       -- Bring names into scope
end MySpace

---

See Also

Skills for detailed coverage:

• lean-fp-basics - Language fundamentals
• lean-fp-monads - Monad details
• lean-tp-tactics - Tactic details
• lean-tp-tactic-selection - Decision trees

Sources:

• Functional Programming in Lean
• Theorem Proving in Lean 4