Lean reference · Math 2001

Introduction: prove it. Elimination: use it. Worked explanations →

This sheet covers the techniques in dayXX.lean and exXX.lean through Day 20. The snippets with ... are proof templates: replace each placeholder with the remaining proof.

Jump to logic, quantifiers, recursion, induction, Lean tactics and techniques, or equality tools.

For the custom logical commands, load macros.lean (or copy the setup in the guide). For the natural-number examples, load natural_numbers.lean: use import natural_numbers locally, or paste its contents at the top of the web editor. It supplies our custom ℕ, plus, times, and their theorems. Type \N for ℕ. Write (2 : ℕ) when the type of a numeral needs to be explicit.

∧ And `\and`

Introduction

From P and Q, conclude P ∧ Q.

p ∧ q

```
apply And.intro
...
```
What Lean needsThe goal P ∧ Q.

What Lean doesReplaces it with two goals, P and Q.
```
conj_intro hpq from hp hq
```
What Lean needshp : P and hq : Q in the context.

What Lean doesAdds hpq : P ∧ Q to the context.
```
have hpq : P ∧ Q := ⟨hp, hq⟩
```
What Lean needshp : P and hq : Q in the context.

What Lean doesAdds hpq : P ∧ Q to the context.

Elimination

From P ∧ Q, conclude P and conclude Q.

p ∧ q

```
conj_elim hp hq from hpq
```
What Lean needshpq : P ∧ Q in the context.

What Lean doesAdds hp : P and hq : Q to the context.
```
have ⟨hp, hq⟩ := hpq
```
What Lean needshpq : P ∧ Q in the context.

What Lean doesAdds hp : P and hq : Q to the context.
```
apply And.elim _ hpq
intro hp hq
...
```
What Lean needshpq : P ∧ Q in the context.

What Lean doesAdds hp : P and hq : Q to the context while retaining the current goal.

∨ Or `\or`

Introduction

From P, conclude P ∨ Q; from Q, conclude P ∨ Q.

p ∨ q

```
disj_intro_left hpq from hp Q
```
What Lean needshp : P in the context.

What Lean doesAdds hpq : P ∨ Q to the context.
```
disj_intro_right hpq from P hq
```
What Lean needshq : Q in the context.

What Lean doesAdds hpq : P ∨ Q to the context.
```
apply Or.intro_left
...
```
What Lean needsThe goal P ∨ Q.

What Lean doesReplaces it with the goal P.
```
apply Or.intro_right
...
```
What Lean needsThe goal P ∨ Q.

What Lean doesReplaces it with the goal Q.
```
apply Or.inl
...
```
What Lean needsThe goal P ∨ Q.

What Lean doesReplaces it with the goal P.
```
apply Or.inr
...
```
What Lean needsThe goal P ∨ Q.

What Lean doesReplaces it with the goal Q.

Elimination

From P ∨ Q, derive the same conclusion from P and from Q.

p ∨ q [p] ⇝ r [q] ⇝ r

```
disj_elim hp hq from hpq
...
```
What Lean needshpq : P ∨ Q in the context.

What Lean doesCreates two copies of the current goal: one with hp : P in the context and one with hq : Q.
```
cases hpq
case inl hp => ...
case inr hq => ...
```
What Lean needshpq : P ∨ Q in the context.

What Lean doesCreates a case with hp : P and a case with hq : Q; both retain the current goal.
```
apply Or.elim hpq
· intro hp
  ...
· intro hq
  ...
```
What Lean needshpq : P ∨ Q in the context.

What Lean doesCreates two copies of the current goal: one under hp : P and one under hq : Q.

→ Implies `\to`

Introduction

To prove P → Q, assume P and derive Q.

[p] ⇝ q

p ⇒ q

```
intro hp
...
```
What Lean needsThe goal P → Q.

What Lean doesAdds hp : P to the context and replaces the goal with Q.

Elimination

From P → Q and P, conclude Q.

p ⇒ qp

```
impl_elim hq from hp hpq
```
What Lean needshpq : P → Q and hp : P in the context.

What Lean doesAdds hq : Q to the context.
```
have hq := hpq hp
```
What Lean needshpq : P → Q and hp : P in the context.

What Lean doesAdds hq : Q to the context.
```
apply hpq
...
```
What Lean needshpq : P → Q in the context and the goal Q.

What Lean doesReplaces the goal with P.

¬ Not `\neg`

Introduction

To prove ¬P, assume P and derive a contradiction.

[p] ⇝ ⊥

¬p

```
change P → False
```
What Lean needsThe goal ¬ P.

What Lean doesRewrites the goal as P → False.
```
change ¬ P at h
```
What Lean needsh : P → False in the context.

What Lean doesRewrites the hypothesis as h : ¬ P.

Elimination

From ¬P and P, derive a contradiction.

¬pp

⊥

```
contradiction
```
What Lean needsContradictory hypotheses, such as hp : P and hnp : ¬ P, in the context.

What Lean doesCloses the current goal.

↔ If and only if `\iff`

Introduction

Prove P → Q and prove Q → P.

p ⇒ qq ⇒ p

p ⇔ q

```
apply Iff.intro
```
What Lean needsThe goal P ↔ Q.

What Lean doesReplaces it with the goals P → Q and Q → P.

Elimination

Use either implication: P → Q or Q → P.

p ⇔ q

p ⇒ q

p ⇔ q

q ⇒ p

```
apply Iff.elim _ h
intro hpq hqp
...
```
What Lean needsh : P ↔ Q in the context.

What Lean doesAdds hpq : P → Q and hqp : Q → P to the context while retaining the current goal.

∀ For every `\forall`

Introduction

For arbitrary t : T, derive P t.

[x ∈ X] ⇝ p(x)

∀x ∈ X, p(x)

```
intro t
...
```
What Lean needsThe goal ∀ x : T, P x.

What Lean doesAdds an arbitrary t : T to the context and replaces the goal with P t.

Elimination

From ∀ x : T, P x, conclude P t for t : T.

∀x ∈ X, p(x)a ∈ X

p(a)

```
have := h t
...
```
What Lean needsh : ∀ x : T, P x and t : T in the context.

What Lean doesAdds this : P t to the context.
```
have hpt := h t
...
```
What Lean needsh : ∀ x : T, P x and t : T in the context.

What Lean doesAdds hpt : P t to the context.

∃ There exists `\exists`

Introduction

Choose t : T and prove P t.

a ∈ Xp(a)

∃x ∈ X, p(x)

```
apply Exists.intro t
...
```
What Lean needsThe goal ∃ x : T, P x and an available term t : T.

What Lean doesChooses t as the witness and replaces the goal with P t.

Elimination

From ∃ x : T, P x, introduce a new t : T and assume P t.

∃x ∈ X, p(x) [a ∈ X], [p(a)] ⇝ q

```
obtain ⟨t, hpt⟩ := h
-- Or:
have ⟨t, hpt⟩ := h
...
```
What Lean needsh : ∃ x : T, P x in the context.

What Lean doesAdds a new witness t : T and hpt : P t to the context.
```
apply Exists.elim h
intro t
intro hpt
...
```
What Lean needsh : ∃ x : T, P x in the context.

What Lean doesAdds a new t : T and hpt : P t to the context while retaining the current goal.

Recursively defined functions

Give the zero and successor values

```
def f : ℕ → ℕ
  | ℕ.zero => ℕ.zero
  | ℕ.succ n => (f n).succ.succ
```
What Lean needsA value at zero and a rule for computing the successor value from f n.

What Lean doesDefines a function that adds two successors at each step. n.succ means ℕ.succ n.
```
def f_match (n : ℕ) : ℕ := match n with
  | .zero => ℕ.zero
  | .succ k => (f_match k).succ.succ
```
What Lean needsThe same zero and successor rules, written with match as in Day 17.

What Lean doesDefines the function by matching the input against the two cases.

Compute, or state the defining equations

```
#eval f 2
```
What Lean needsA defined function and a concrete input.

What Lean doesComputes the value and displays it. Our custom ℕ may display its zero/successor constructors. This is a computation, not a proof for all inputs.
```
theorem f_zero : f ℕ.zero = ℕ.zero := by
  rfl

theorem f_succ (n : ℕ)
    : f n.succ = (f n).succ.succ := by
  rfl
```
What Lean needsThe definition of f above.

What Lean doesProves and names the defining equations so that later proofs can use rewrite [f_zero] or rewrite [f_succ].

The course file already defines plus and times recursively on their first input. Write them as m + n and m * n; parentheses specify grouping when needed.

Induction on our natural numbers

The two cases

```
intro n  -- If the goal starts with ∀ n : ℕ, ...
induction n using ℕ.rec
case zero =>
  ...
case succ n ih =>
  ...
```
What Lean needsn : ℕ and a goal about n, say P n.

What Lean doesCreates the base goal P ℕ.zero and the successor goal P n.succ, with ih : P n available in the successor case.

Use the induction hypothesis for n to prove the statement for n.succ. It is available only in the successor case. Choose the induction variable to match the input on which the function recurses.

A complete example from addition

```
example (n : ℕ) : n + ℕ.zero = n := by
  induction n using ℕ.rec
  case zero =>
    unfold plus
    rfl
  case succ n ih =>
    unfold plus
    rewrite [ih]
    rfl
```
What Lean needsThe course definition of plus.

What Lean doesIn the successor case, exposes (n + ℕ.zero).succ = n.succ, replaces n + ℕ.zero using ih, then finishes the identical sides with rfl.

Lean tactics and techniques

Adding facts

Use assumptions to obtain new facts, prove an intermediate statement, or open the assumptions in each case.

```
have hpt := h t
-- Without a name:
have := h t
exact this
```
What Lean needsh : ∀ x : T, P x and t : T.

What Lean doesAdds the specialized fact. An unnamed have calls the new fact this.
```
have h₁ : ∃ x : T, P x := by
  apply Exists.intro t
  exact hpt
...
```
What Lean needsAn available t : T and hpt : P t.

What Lean doesProves an intermediate statement in an indented block, then adds h₁ and returns to the original goal.
```
rcases hpq with hp | hq
· ...
· ...
```
What Lean needshpq : P ∨ Q, as in ex14.lean.

What Lean doesCreates one branch with hp : P and another with hq : Q.

Simplifying goals

Work backward from the goal, split it into smaller goals, or finish it with a known fact. Dots and show help organize the proof; sorry is a temporary placeholder.

```
exact h
-- For example: exact h t, or exact hpq hp
```
What Lean needsThe fact or expression supplied has the type of the current goal.

What Lean doesCloses that goal. Arguments can specialize a universal statement or use an implication.
```
exact ⟨hp, hq⟩
-- For an existential: exact ⟨t, hpt⟩
```
What Lean needsA conjunction goal with proofs of both parts, or an existential goal with a witness and its proof.

What Lean doesBuilds the required conjunction or existential statement and closes the goal.
```
apply And.intro
· exact hp
· exact hq
```
What Lean needsThe goal P ∧ Q, with hp : P and hq : Q.

What Lean doesEach · focuses on one goal; its indented proof must finish that goal. Type \. for the dot.
```
show P → Q
intro hp
...
```
What Lean needsA goal that can already be written as P → Q.

What Lean doesDisplays the intended goal explicitly before continuing the proof.
```
sorry
```
What Lean needsAn unfinished proof while you are working.

What Lean doesAccepts a placeholder with a warning. Put the cursor here to inspect the goal; replace it to finish the proof.
```
apply h.mp
-- In the other direction: apply h.mpr
```
What Lean needsh : P ↔ Q and the goal Q (or P for mpr).

What Lean doesUses the forward implication and leaves P to prove; mpr uses the reverse implication and leaves Q.
```
simp [hp, hq]
```
What Lean needsKnown truth values, such as hp : P and hq : Q, in a truth-table case (Day 12).

What Lean doesSimplifies the logical goal using these facts and Lean's usual simplification rules; it closes the goal if the result is settled.
```
simp only [succ_times, times_succ]
simp only [plus_assoc, plus_comm]
```
What Lean needsA goal to simplify using the listed equalities, as in Days 19–20.

What Lean doesRepeatedly simplifies using the supplied rules. In these examples the second list rearranges sums into a common form. It may close the goal.

simp only keeps the theorem list explicit; simp [hp, hq] also uses Lean's usual simplification rules. Use rewrite when you want to control a particular substitution and its direction.

Equality: definitions and rewriting

Use a definition or equality

```
rfl
```
What Lean needsAn equality whose sides are the same after computing definitions, such as f ℕ.zero = ℕ.zero.

What Lean doesCloses the equality goal. An algebraic identity may need rewriting or induction first.
```
unfold f
```
What Lean needsAn occurrence of the defined function f in the goal.

What Lean doesExpands its definition. At zero or a successor this exposes the corresponding rule.
```
rewrite [ih]
rewrite [zero_plus, plus_zero]
rewrite [← plus_assoc a b c]
```
What Lean needsAn equality hypothesis or theorem and a matching expression. Supply arguments to select the instance; type \l for ←.

What Lean doesReplaces a matching left side by its right side. ← reverses the direction; a list performs the rewrites in order. Finish with rfl when both sides match.
```
change ℕ.zero.succ.succ * n = n + n
```
What Lean needsThe goal (2 : ℕ) * n = n + n.

What Lean doesDisplays the same goal using the successor notation for two. change must preserve the goal by definitions alone.
```
rewrite [show (2 : ℕ) = ℕ.zero.succ.succ by rfl]
```
What Lean needsA matching numeral in the goal.

What Lean doesProves a small equality inline and uses it immediately to rewrite.

Focus on part of an equality

```
conv => lhs ; unfold plus
```
What Lean needsAn equality with an occurrence of plus on its left side.

What Lean doesFocuses on the left side and unfolds there. Use rhs to focus on the right side.
```
conv => rhs ; arg 1 ; change (1 : ℕ) + n
```
What Lean needsAn equality with right side n.succ + t, as in Day 20.

What Lean doesSelects the right side, then its first argument n.succ, and writes that argument as (1 : ℕ) + n.
```
apply congrArg
```
What Lean needsAn equality with the same outer function on both sides, such as a.succ = b.succ or n + a = n + b.

What Lean doesReduces the goal to equality of the inputs, a = b, as in the multiplication proofs in ex18.lean.

∧ And \and

Introduction

Elimination

∨ Or \or

Introduction

Elimination

→ Implies \to

Introduction

Elimination

¬ Not \neg

Introduction

Elimination

↔ If and only if \iff

Introduction

Elimination

∀ For every \forall

Introduction

Elimination

∃ There exists \exists

Introduction

Elimination

Recursively defined functions

Give the zero and successor values

Compute, or state the defining equations

Induction on our natural numbers

The two cases

A complete example from addition

Lean tactics and techniques

Adding facts

Simplifying goals

Equality: definitions and rewriting

Use a definition or equality

Focus on part of an equality

∧ And `\and`

∨ Or `\or`

→ Implies `\to`

¬ Not `\neg`

↔ If and only if `\iff`

∀ For every `\forall`

∃ There exists `\exists`