Module 2 · Lesson 4

exact & apply

exact provides a proof term directly. applyuses a lemma or hypothesis that might need additional arguments. Together, they form the foundation of how you provide proofs in Lean.

exact: Direct Proof

Use exact when you have exactly what you need to prove the goal. Think of it as saying "here is the proof—done!"

lean

1example (h : 2 + 2 = 4) : 2 + 2 = 4 := by
2  exact h
3  -- h has exactly the type we need
4
5example : True := by
6  exact trivial
7  -- trivial : True
8
9example (a b : Nat) (h : a = b) : a = b := by
10  exact h

exact closes the goal immediately. If the provided term doesn't have the right type, Lean gives an error.

When to Use exact

You have a hypothesis with the exact goal type: exact h
You know the library lemma and all its arguments: exact Nat.add_comm a b
You want to be explicit: Unlike assumption, you name exactly what you're using

Using exact with Library Lemmas

lean

1example (n : Nat) : n + 0 = n := by
2  exact Nat.add_zero n
3  -- Nat.add_zero : ∀ n, n + 0 = n
4  -- Applied to n gives: n + 0 = n ✓
5
6example (a b : Nat) : a + b = b + a := by
7  exact Nat.add_comm a b
8
9example : ∀ n : Nat, n = n := by
10  exact fun n => rfl

Key Takeaway

exact e succeeds when e has exactly the same type as the goal. It's like saying "here is the proof."

apply: Working Backwards

apply is like exact, but it can leave "holes" for arguments you don't have yet. It works backwards from the goal:

lean

1example (a b c : Nat) (hab : a = b) (hbc : b = c) : a = c := by
2  apply Eq.trans
3  -- Eq.trans : a = b → b = c → a = c
4  -- Goal 1: a = ?middle
5  -- Goal 2: ?middle = c
6  · exact hab   -- Provide first equality
7  · exact hbc   -- Provide second equality

apply works backwards from the goal. If a lemma says "A → B" and your goal is B, apply creates a new goal: prove A.

When to Use apply

The lemma's conclusion matches your goal: But you need to provide its premises
You're building a proof backwards: From goal to subgoals
You want Lean to infer some arguments: Unlike exact, you don't need to provide everything

apply with Implications

lean

1example (h : 1 = 1 → 2 = 2) : 2 = 2 := by
2  apply h
3  -- Goal becomes: 1 = 1
4  rfl
5
6example (P Q : Prop) (h : P → Q) (hp : P) : Q := by
7  apply h
8  -- Goal becomes: P
9  exact hp

exact vs apply

lean

1-- When the lemma fits exactly, both work:
2example (n : Nat) : n + 0 = n := by
3  exact Nat.add_zero n
4
5example (n : Nat) : n + 0 = n := by
6  apply Nat.add_zero
7  -- Lean infers n from the goal
8
9-- But apply is more flexible:
10example (a b c : Nat) (h : a = b) : a + c = b + c := by
11  apply congrArg (· + c)
12  -- Creates goal: a = b
13  exact h

ℹ

exact requires you to fill in all arguments.apply lets Lean infer what it can and creates subgoals for the rest.

Common Mistakes

Mistake 1: Using exact when you need apply

lean

1-- ❌ Won't work: Nat.add_comm needs two arguments
2-- example (a b : Nat) : a + b = b + a := by
3--   exact Nat.add_comm  -- Missing arguments!
4
5-- ✓ Correct: provide the arguments
6example (a b : Nat) : a + b = b + a := by
7  exact Nat.add_comm a b
8
9-- ✓ Or let apply infer them
10example (a b : Nat) : a + b = b + a := by
11  apply Nat.add_comm

Mistake 2: Forgetting that apply creates subgoals

lean

1example (P Q R : Prop) (hpq : P → Q) (hqr : Q → R) (hp : P) : R := by
2  apply hqr
3  -- Goal is now Q, not R!
4  -- You still need to prove Q
5  apply hpq
6  exact hp

Mistake 3: Wrong order of apply

lean

1-- When chaining implications, apply in reverse order
2example (P Q R : Prop) (f : P → Q) (g : Q → R) : P → R := by
3  intro hp
4  -- Goal: R
5  apply g   -- Goal becomes: Q  
6  apply f   -- Goal becomes: P
7  exact hp

Common Patterns

Using Hypotheses

lean

1example (P Q R : Prop) (hpq : P → Q) (hqr : Q → R) (hp : P) : R := by
2  apply hqr
3  -- Goal: Q
4  apply hpq
5  -- Goal: P
6  exact hp

Transitivity

lean

1example (a b c d : Nat) (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d := by
2  apply Eq.trans
3  · apply Eq.trans
4    · exact h1
5    · exact h2
6  · exact h3
7
8-- Or more concisely:
9example (a b c d : Nat) (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d := by
10  exact Eq.trans (Eq.trans h1 h2) h3

Congruence

lean

1-- If a = b, then f a = f b
2example (f : Nat → Nat) (a b : Nat) (h : a = b) : f a = f b := by
3  apply congrArg
4  exact h
5
6-- Or just:
7example (f : Nat → Nat) (a b : Nat) (h : a = b) : f a = f b := by
8  rw [h]

The assumption Tactic

assumption searches your hypotheses for an exact match:

lean

1example (P Q : Prop) (hp : P) (hq : Q) : P := by
2  assumption
3  -- Automatically finds hp : P
4
5example (a b : Nat) (h1 : a = b) (h2 : b = a) : b = a := by
6  assumption
7  -- Finds h2

Deep Dive: Unification

When you write apply lemma, Lean performsunification—it tries to match the conclusion of the lemma with your goal, figuring out what values the lemma's arguments must have.

lean

1-- Goal: 5 + 0 = 5
2-- Lemma: Nat.add_zero : ∀ n, n + 0 = n
3
4-- apply Nat.add_zero unifies:
5-- n + 0 = n  with  5 + 0 = 5
6-- Solution: n = 5

If unification fails (the lemma doesn't match), applygives an error.

exact? and apply?

Not sure which lemma to use? Let Lean search:

lean

1example (n : Nat) : n + 0 = n := by
2  exact?
3  -- Suggests: exact Nat.add_zero n
4
5example (a b : Nat) : a + b = b + a := by
6  apply?
7  -- Suggests: exact Nat.add_comm a b

These tactics search Lean's library for lemmas that might work. Very useful for discovering what's available!

Exercise 1: Use apply

Use apply with Nat.add_comm to close the goal.

lean

1example (a b : Nat) : a + b = b + a := by
2  apply Nat.add_comm

Exercise 2: Chain apply

Use apply twice to prove this implication chain.

lean

1example (P Q R : Prop) (f : P → Q) (g : Q → R) (hp : P) : R := by
2  apply g
3  apply f
4  exact hp

Exercise 3: exact with Library Lemma

Use exact with the right lemma and arguments.

lean

1example (n : Nat) : 0 + n = n := by
2  exact Nat.zero_add n

Summary

Tactic	Use When
exact e	You have exactly what you need
apply lemma	Lemma's conclusion matches goal
assumption	Goal matches a hypothesis exactly
exact?	Search for matching lemma

simp — Simplification Next: intro — Assumptions