Lean reference · Math 2001

∧ And `\and`

Introduction

From P and Q, conclude P ∧ Q.

pq

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

p

p ∧ q

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

p ∨ q

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

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

q

```
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

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.

Functions: definitions and extensionality

These examples use the course definitions in project/solutions/functions.lean: compose g f := fun x => g (f x), written g ∘ f. Thus f is applied first. Load that file locally with import functions, or paste its contents into the web editor.

Define a function; prove functions equal

```
def subtype_value {S : Type} {P : S → Prop}
    : {a : S // P a} → S := by
  intro x
  exact x.val
```
What Lean needsA function type A → B to construct.

What Lean doesintro x introduces the input; the remaining goal asks for an output of type B. A direct definition can instead use fun x => x.val.
```
example {S T U V : Type} (f : S → T)
    (g : T → U) (h : U → V)
    : h ∘ (g ∘ f) = (h ∘ g) ∘ f := by
  funext x
  unfold compose
  rfl
```
What Lean needsAn equality between functions with the same domain and codomain.

What Lean doesfunext x introduces an arbitrary input and reduces equality of functions to equality of their values at that input. Here both sides reduce to h (g (f x)).

Use injectivity, surjectivity, and inverse equations

```
unfold injective
intro x y hxy
...

-- For a surjectivity goal:
unfold surjective
intro t
apply Exists.intro s
...
```
What Lean needsA goal injective f, or surjective f and a chosen preimage s.

What Lean doesInjectivity leaves x = y with hxy : f x = f y. Surjectivity leaves f s = t. For bijective f, unfold bijective and prove both parts. Use unfold injective at h to expose a hypothesis; unfold injective at ⊢ h unfolds in both the goal and h.

example {S T : Type} {f : S → T} {g : T → S}
    (h : g ∘ f = id) : surjective g := by
  unfold surjective
  intro x
  apply Exists.intro (f x)
  change (g ∘ f) x = id x
  rewrite [h]
  rfl

What Lean needsA function equality h : g ∘ f = id.

What Lean doeschange displays the goal in a definitionally equal form where rewrite [h] can use the inverse equation.

Subtypes: values together with proofs

{a : S // P a} is the type of values a : S accompanied by a proof of P a. Unlike ∃ a : S, P a, it is a type of data. Course examples include ℕ_pos, Evens, and image f. Type \< and \> for ⟨ and ⟩.

Construct a member

```
example {S : Type} {P : S → Prop}
    (a : S) (ha : P a) : {x : S // P x} := by
  apply Subtype.mk
  case val => exact a
  case property => exact ha
```
What Lean needsA subtype goal, a candidate value a, and a proof ha of its required property.

What Lean doesSubtype.mk asks for the underlying value and then a proof that it satisfies the property. The second goal depends on the value supplied in the first.
```
example {S : Type} {P : S → Prop}
    (a : S) (ha : P a) : {x : S // P x} := by
  exact ⟨a, ha⟩
  -- Equivalently: exact Subtype.mk a ha
```
What Lean needsThe same value and property proof.

What Lean doesBuilds the subtype member directly. The expected type tells Lean what the angle brackets construct.

Unpack a member; prove members equal

example {S : Type} {P : S → Prop}
    (x : {a : S // P a}) : P x.val := by
  exact x.property

example {S : Type} {P : S → Prop}
    (x : {a : S // P a}) : ∃ a : S, P a := by
  have ⟨a, ha⟩ := x
  exact ⟨a, ha⟩

example {S : Type} {P : S → Prop}
    : {a : S // P a} → S := by
  intro ⟨a, ha⟩
  exact a

What Lean needsA subtype member x, or a function goal whose input is a subtype member.

What Lean doesx.val : S is its underlying value and x.property : P x.val is its proof. have ⟨a, ha⟩ := x unpacks an existing member; intro ⟨a, ha⟩ unpacks an input as it is introduced. A named subtype may need unfold Evens at x first.

```
example {S : Type} {P : S → Prop}
    (x y : {a : S // P a})
    (h : x.val = y.val) : x = y := by
  apply Subtype.ext
  exact h
```
What Lean needsAn equality goal between two members of the same subtype.

What Lean doesapply Subtype.ext reduces the goal to equality of their underlying values. No equality of the property proofs is required. After constructing or unpacking members, dsimp (or simp) can simplify projections such as (Subtype.mk a ha).val.

Axiom of choice: choose and choose_spec

Write open Classical to use the short names below; the full names are Classical.choose and Classical.choose_spec. Unpacking an existential with have ⟨a, ha⟩ := h suffices inside a proof of a proposition. Choice also lets us select data from existence proofs, such as a preimage for every output of a surjection.

Select a witness and its property

```
open Classical

example {S : Type} {P : S → Prop}
    (h : ∃ a : S, P a) : P (choose h) := by
  let a := choose h
  have ha : P a := choose_spec h
  exact ha
```
What Lean needsAn existence proof h : ∃ a : S, P a.

What Lean doeschoose h : S selects a witness; choose_spec h proves P (choose h). let names a value, while have names a proof. This is a term choose h, rather than the separate choose tactic.

Build a right inverse of a surjection

```
open Classical

noncomputable def chosen_right_inverse
    {S T : Type} {f : S → T} (h : surjective f)
    : {g : T → S // f ∘ g = id} := by
  let g (t : T) := choose (h t)
  have hg (t : T) : f (g t) = t :=
    choose_spec (h t)
  apply Subtype.mk
  case val => exact g
  case property =>
    funext t
    change f (g t) = t
    exact hg t
```
What Lean needsA surjectivity proof h; for each t, h t : ∃ s, f s = t.

What Lean doesDefines g by choosing a preimage for each t. The parameterized have hg (t : T) records its property for every input. funext proves the right inverse equation. A definition that uses choice to produce data needs noncomputable; a theorem asserting that such an inverse exists does not.

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

Functions: definitions and extensionality

Define a function; prove functions equal

Use injectivity, surjectivity, and inverse equations

Subtypes: values together with proofs

Construct a member

Unpack a member; prove members equal

Axiom of choice: choose and choose_spec

Select a witness and its property

Build a right inverse of a surjection

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`