Lean 4 Phrasebook: Mathematical English to Lean

This guide translates common mathematical proof phrases into their Lean 4 equivalents, helping you think in natural mathematical language while writing formal proofs.

Inspiration: This phrasebook is inspired by Terence Tao's Lean Phrasebook, reorganized by proof pattern with additional context and explanations.

Validation: Patterns in this guide are based on Tao's phrasebook (which was created for Lean 4) and follow current Lean 4 syntax. While most patterns should work with modern mathlib, specific lemma names may evolve. When in doubt, use exact? or apply? to find current mathlib lemmas.

Quick Reference by Situation

You want to...

Introduce assumptions: intro, rintro, by_cases
Use hypothesis: exact, apply, rw, simp [h]
Split goal: constructor, refine ⟨?_, ?_⟩, left/right
Split hypothesis: rcases, obtain, cases
Add intermediate fact: have, obtain
Change perspective: suffices, convert, change
Prove by contradiction: by_contra, contrapose!
Chain equalities: calc, rw [h₁, h₂]
Simplify: simp, ring, field_simp, norm_num
Explore options: exact?, apply?, simp?
Manage goals: swap, pick_goal n, rotate_left, all_goals

See also: tactics-reference.md for comprehensive tactic documentation.

Forward Reasoning
Backward Reasoning
Case Analysis
Rewriting and Simplification
Equational Reasoning
Working with Quantifiers
Working with Connectives
Contradiction and Contrapositive
Inequalities and Ordering
Set Theory
Extensionality
Algebraic Reasoning
Goal Management
Advanced Patterns

Forward Reasoning

Building up facts from what you know.

Stating Intermediate Claims

"Observe that A holds because of reason r"

have h : A := by r

Can omit h - result becomes this by default
If r is one-liner: have h : A := r

"We claim that A holds. [proof]"

have h : A := by
  <proof of A>

"Observe that X equals Y by definition"

have : X = Y := rfl

Alternative: have : X = Y := by rfl

"From hypothesis h, applying f gives us B"

have hB : B := f h

Using Hypotheses

"The claim follows from hypothesis h"

assumption
-- or: exact h

"This follows by definition"

rfl

"This follows from reason r"

exact r
-- Explore: exact?

Replacing Hypotheses

"By f, we replace hypothesis A with B"

replace h := f h

"We replace hypothesis A with B using this argument"

replace h : B := by <proof>

Discarding Hypotheses

"Hypothesis h is no longer needed"

clear h

"We only need hypotheses A and B going forward"

clear_except hA hB

Backward Reasoning

Working from the goal backwards.

Reducing the Goal

"By A, it suffices to show..."

apply A

"It suffices to show B [proof of B], then we get our goal [proof using B]"

suffices h : B by
  <proof of goal using h>
<proof of B>

Alternative: have h : A; swap to prove A later

"Suppose P holds [arguments]. In summary, P implies Q."

have hPQ (hP : P) : Q := by
  <arguments reaching conclusion>
  exact hQ

Use ?Q if you want Lean to infer the conclusion type

"Later we'll prove A. Assuming it for now..."

suffices h : A from
  <proof assuming h>
<proof of A>

"We conjecture that A holds"

theorem A_conj : A := by sorry
-- Inside proofs: have h : A := by sorry

Converting Goals

"We reduce to showing B [proof it suffices], now show B [proof of B]"

suffices B by
  <proof original goal given B>
<proof of B>

If B is very close to goal, try convert tactic
If B is definitionally equal, use change

"We need to show A'"

show A'

Finds matching goal among multiple goals
Moves it to front of goal queue

"By definition, the goal rewrites as A'"

change A'

Also works for hypotheses: change A' at h

Case Analysis

Breaking proofs into separate cases.

Disjunction (Or)

"Hypothesis h says A or B. We split into cases."

rcases h with hA | hB
<proof using hA>
<proof using hB>

"It suffices to prove A [to get A ∨ B]"

left    -- or: Or.inl

"It suffices to prove B [to get A ∨ B]"

right   -- or: Or.inr

Boolean Dichotomy

"We split into cases depending on whether A holds."

by_cases h : A
<proof assuming h : A>
<proof assuming h : ¬A>

Alternative using law of excluded middle:

rcases em A with hA | hnA

Inductive Types

"We split cases on natural number n: base case n=0, step case n=m+1."

rcases n with _ | m
<proof for n = 0>
<proof for n = m+1, with m available>

Works for any inductive type

"We perform induction on n."

induction n with
| zero => <proof of base case>
| succ n ih => <proof of inductive step, with ih : P n available>

Pattern Matching

"We divide into cases n=0, n=1, and n≥2."

match n with
| 0 => <proof for 0>
| 1 => <proof for 1>
| n+2 => <proof for n+2>

Rewriting and Simplification

Transforming expressions using equalities.

Basic Rewriting

"We rewrite the goal using hypothesis h"

rw [h]

Reverse direction: rw [← h]
Multiple rewrites: rw [h₁, h₂, h₃]
Close proof if rewrite produces assumption: rwa [h]

"We rewrite using A (which holds by r)"

rw [show A by r]
-- Alternative: rw [(by r : A)]

"We replace X by Y, using proof r that they're equal"

rw [show X = Y by r]

"Applying f to both sides of h : X = Y"

apply_fun f at h    -- produces h : f X = f Y

Alternative: replace h := congr_arg f h
Alternative: replace h := by congrm (f $h)
For adding 1 to both sides: congrm (1 + $h)

"We need associativity before rewriting"

assoc_rw [h]

"Rewrite at position n only"

nth_rewrite n [h]

Simplification

"We simplify using hypothesis h"

simp [h]

Multiple simplifications: simp [h₁, h₂, ...]
More targeted: simp only [hypotheses]
Explore options: simp?
Simplify to assumption: simpa

"We simplify hypothesis A"

simp at h

Works with [hypotheses], simp only, etc.
Can use wildcard: simp at *

"By definition, this rewrites as"

dsimp

More restrictive than simp - only definitional equalities

"Expanding all definitions"

unfold

For specific definition: unfold foo
Also works on hypotheses: unfold at h
Only definitional: dunfold

Field Operations

"In a field, we simplify by clearing denominators"

field_simp [hypotheses]

Often followed by ring
Automatically finds non-zero denominators or creates goals
Works on hypotheses: field_simp [hypotheses] at h

Equational Reasoning

Chains of equalities and inequalities.

Calculation Chains

"We compute: x = y (by r₁), = z (by r₂), = w (by r₃)"

calc x = y := by r₁
   _ = z := by r₂
   _ = w := by r₃

Also handles chained inequalities: ≤, <, etc.
gcongr is useful for inequality steps

"We rewrite using the algebraic identity (proven inline)"

rw [show ∀ x : ℝ, ∀ y : ℝ, (x+y)*(x-y) = x*x - y*y by intros; ring]

Working with Quantifiers

Universal and existential quantification.

Universal Introduction

"Assume A implies B. Thus suppose A holds."

intro hA

Can omit name - becomes this
For complex patterns: rintro with pattern matching

"Let x be an element of X."

intro x hx    -- for goal: ∀ x ∈ X, P x

Universal Elimination

"Since a ∈ X and ∀ x ∈ X, P(x) holds, we have P(a)"

have hPa := h a ha

Can use h a ha directly anywhere instead of naming it
Can also use specialize h a ha (but this replaces h)

Existential Introduction

"We take x to equal a [to prove ∃ x, P x]"

use a

Existential Elimination

"By hypothesis, there exists x satisfying A(x)"

rcases h with ⟨x, hAx⟩
-- Alternative: obtain ⟨x, hAx⟩ := h

"From nonempty set A, we arbitrarily select element x"

obtain ⟨x⟩ := h    -- where h : Nonempty A

"Using choice, we select a canonical element from A"

let x := h.some          -- where h : Nonempty A
-- Alternatives: x := h.arbitrary
--               x := Classical.choice h

Working with Connectives

Conjunction, disjunction, and equivalence.

Conjunction (And)

"To prove A ∧ B, we prove each in turn."

constructor
<proof of A>
<proof of B>

For more than two: refine ⟨?_, ?_, ?_, ?_⟩

"By hypothesis h : A ∧ B, we have both A and B"

rcases h with ⟨hA, hB⟩
-- Alternative: obtain ⟨hA, hB⟩ := h

Can also use projections: h.1 and h.2
Multiple conjuncts: obtain ⟨hA, hB, hC, hD⟩ := h

"An intro followed by rcases can be merged"

rintro ⟨hA, hB⟩    -- instead of: intro h; rcases h with ⟨hA, hB⟩

Equivalence (Iff)

"To prove A ↔ B, we prove both directions."

constructor
<proof of A → B>
<proof of B → A>

Contradiction and Contrapositive

Proof by contradiction and contrapositive.

Contradiction

"We seek a contradiction"

exfalso

"But this is absurd [given h : A and nh : ¬A]"

absurd h nh

Can derive A or ¬A directly using show A by r to save steps

"Given A and ¬A, this gives the required contradiction"

contradiction

"Suppose for contradiction that A fails [to prove A]"

by_contra nh

"Suppose for contradiction that A holds [to prove ¬A]"

intro hA

"Suppose Y < X [to prove X ≤ Y by contradiction]"

by_contra h
simp at h

Contrapositive

"Taking contrapositives, it suffices to show ¬A implies ¬B"

contrapose! h    -- where h : B, goal is A
-- Result: h : ¬A, goal is ¬B

Inequalities and Ordering

Working with partial orders and inequalities.

Basic Transitions

"Given h : X ≤ Z, to prove X ≤ Y it suffices to show Z ≤ Y"

apply h.trans
-- Alternative: apply le_trans h

"Given h : X ≤ Z, to prove X < Y it suffices to show Z < Y"

apply h.trans_lt

"Given h : Z ≤ Y, to prove X ≤ Y it suffices to show X ≤ Z"

apply le_trans _ h

"Given h : X ≤ X' and h' : Y' ≤ Y, to prove X ≤ Y suffices to show X' ≤ Y'"

apply le_trans _ (le_trans h _)

Rewrites with Inequalities

"Given h : X = Z, to prove X ≤ Y suffices to show Z ≤ Y"

rw [h]

"Given h : Z = Y, to prove X ≤ Y suffices to show X ≤ Z"

rw [← h]

Antisymmetry

"To prove x = y, show x ≤ y and y ≤ x"

apply le_antisymm

Order Isomorphisms

"To prove X ≤ Y, suffices to show f(X) ≤ f(Y) where f is order iso"

apply_fun f

Algebraic Manipulations

"To prove X ≤ Y, suffices to show X + Z ≤ Y + Z"

rw [← add_le_add_right]

Many variants: add_le_add_left, sub_le_sub_right, etc.

"To prove X ≤ Y, suffices to show X·Z ≤ Y·Z (with Z > 0)"

apply mul_le_mul_right

Congruence for Inequalities

"To prove x + y ≤ x' + y', show x ≤ x' and y ≤ y'"

gcongr

Works well with calc blocks
For sums/products with indices: gcongr with i hi

"Given h : X' ≤ Y', to prove X ≤ Y show X = X' and Y = Y'"

convert h using 1

Works for many relations beyond ≤
Can adjust conversion depth: using 2, etc.

Positivity

"This expression is clearly positive from hypotheses"

positivity

Works for goals: x > 0 or x ≥ 0

Set Theory

Working with sets, subsets, and set operations.

Subset Proofs

"To prove X ⊆ Y: let x ∈ X, show x ∈ Y"

intro x hx

"To prove X = Y: show X ⊆ Y and Y ⊆ X"

apply Set.Subset.antisymm

Set Operations

"x ∈ X ∪ Y means x ∈ X or x ∈ Y"

-- Intro: left (or right)
-- Elim: rcases h with hX | hY
rintro hX | hY

"x ∈ X ∩ Y means x ∈ X and x ∈ Y"

rintro ⟨hX, hY⟩

Extensionality

Proving equality by extensionality.

Function Extensionality

"To prove f = g, show f(x) = g(x) for all x"

ext x

Set Extensionality

"To prove S = T, show x ∈ S ↔ x ∈ T for all x"

ext x

Congruence

"Given f(x) = f(y), to prove goal it suffices to show x = y"

congr

Sometimes congr! works better
Control depth: congr 1, congr 2, etc.
More precise: congrm

"To prove Finset.sum X f = Finset.sum X g, show f(x) = g(x) for all x ∈ X"

apply Finset.sum_congr rfl

If summing over different sets Y: replace rfl with proof X = Y

Algebraic Reasoning

Automatic tactics for algebra.

Ring Theory

"This follows from ring axioms"

ring

"This follows from the laws of linear inequalities"

linarith

Logical Tautologies

"This follows by logical tautology"

tauto

Numerical Verification

"Which can be verified numerically"

norm_num

Type Casting

"Expression is the same whether x is viewed as ℕ or ℝ"

norm_cast

Rearranging Terms

"Move all a terms left, all b terms right"

move_add [← a, b]

For products: move_mul [← a, b]

Goal Management

Managing multiple goals and proof structure.

Goal Manipulation

"We prove the latter goal first"

swap

Also: pick_goal n (bring goal n to the front), rotate_left n / rotate_right n. swap n and bare rotate are not Lean 4 tactics.

"We establish all these goals by the same argument"

all_goals { <tactics> }

Use try { <tactics> } for goals where some might fail
Drop braces for single tactic: all_goals tactic

Negation Manipulation

"Pushing negation through quantifiers"

push_neg

Symmetry

"To prove X = Y, we rewrite as Y = X"

symm

Advanced Patterns

More sophisticated proof techniques.

Without Loss of Generality

"Without loss of generality, assume P"

wlog h : P
<proof assuming ¬P and that goal holds given P>
<proof assuming P>

Can generalize variables: wlog h : P generalizing ...

Abbreviations and Definitions

"Let X denote the quantity Y"

let X := Y

"We abbreviate expression Y as X"

set X := Y

Actively replaces all Y with X
Track equality: set X := Y with h gives h : X = Y
Make X independent variable: generalize : Y = X or generalize h : Y = X

Automation Tactics

"One is tempted to try..."

apply?

"To conclude, one could try"

exact?

Filter Reasoning

"For ∀ᶠ x in f, Q x given ∀ᶠ x in f, P x: show Q x when P x holds"

filter_upwards [h]

Can combine multiple filter hypotheses: filter_upwards [h, h']

Conditional Expressions

"For goal involving (if A then x else y), split cases"

split
<proof if A is true>
<proof if A is false>

Proof Architecture Patterns

Organizing complex proofs.

Delayed Proofs

"We claim A [use it], later we prove A"

have h : A
swap
<use h>
<prove h>

Proof Summaries

"We perform the following argument [details]. In summary, P holds."

have hP : ?P := by
  -- (arguments reaching conclusion)
  exact hP

"Let n be a natural number [arguments]. In summary, P(n) holds for all n."

have hP (n : ℕ) : ?P := by
  -- (arguments using n)
  exact hP

/lean4

lean4referenceslean-phrasebook.md