Lean, one tactic at a time

Reading a Lean proof is hard because the proof text hides the one thing that matters: the goal Lean is looking at between lines. Here you write proofs yourself, one tactic at a time, and see Lean's goal change after each one. Every module starts with a worked example to step through, then gives you exercises to solve. Wrong moves show Lean's real error message, with a plain-English reading of it.

Follows the tactic chapters of Theorem Proving in Lean 4 by Avigad, de Moura, Kong and Ullrich (free online), Chapters 3–5 and 7–8; the exercises are written for this page. Every goal, accepted move and error message here was produced by running Lean on the exercises and on about 2,000 tactics a learner might type, across 338 goal states, with no Mathlib, so the page can't drift from what Lean really does. When you type something it didn't record, it says so rather than guess; Open in the Lean editor then takes your proof so far to the official online editor, where real Lean checks anything. Once these feel easy, the walkthroughs in Proof Paths are readable.

Write it yourselfTPIL Ch. 3 and 5

Reading the goal view

Everything in Lean happens against a goal: what you have, and what you must show. Learn to read that panel and most of Lean stops being mysterious, because each tactic is just a way of changing it.

The idea

A statement. example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by reads: "for any propositions p and q, given a proof hp of p and a proof hq of q, here is a proof of p ∧ q". Everything before the last colon is given; after it is the claim; by starts a list of tactics. (theorem name … := is the same thing with a name.)

The goal view. Lean turns that into a goal. Above the ⊢ are the hypotheses, each written name : what it says. After ⊢ is what you must prove. Read hp : p as "hp is a proof of p".

Tactics change the goal. A tactic either closes the goal, or replaces it with new goals (often easier, sometimes several). When there are several, tactics act on the first one shown. The proof is finished when no goals remain.

Three tactics are enough to start: exact h ("this hypothesis is exactly the goal"), rfl ("both sides are literally the same, after computing"), and constructor ("split the goal into its parts", e.g. both halves of an ∧).

Typing symbols: the buttons under the box insert them, or type what you would in a Lean editor: \< for ⟨, \> for ⟩, \l for ←, \and, \or, \not, \ex, \all, followed by a space.

Watch

Your turn

Check your understanding

In the goal view, what is h in the line h : a = b?

The name of a hypothesis: a proof that a = b, which you may use.
A variable whose value is a = b.Close, but it's a proof of the statement, not the statement's value. You use it with exact h, rw [h] and so on.
Something you still have to prove.What you have to prove comes after ⊢. Above it is what you're given.

Lean treats a proof as a kind of object with a type, and the type is the statement it proves. That is why the same name : type notation is used for numbers (n : Nat) and for proofs (h : a = b).

After constructor Lean shows two goals, left and right. You type exact hp. What does it try to prove?

The first goal shown, left
Whichever goal hp fitsLean doesn't search: tactics act on the first goal, and if hp doesn't fit it you get a type mismatch.
Both goals at onceOnly tactics written to act on all goals (like all_goals) do that.

Try it in the third exercise: type exact hp right after constructor and read the error.

Practice in the Lean editor

A triple ∧One anonymous constructor for nested pairs

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ (q ∧ r) := by
  sorry

Hint

⟨a, b⟩ builds a pair; ⟨a, b, c⟩ is shorthand for ⟨a, ⟨b, c⟩⟩.

Solution

  exact ⟨hp, hq, hr⟩

Or constructor, exact hp, constructor, exact hq, exact hr. Both are checked by Lean.

Write it yourselfTPIL Ch. 3 and 4

→ and ∀: intro and apply

An implication is proved by assuming its left side, and used by working backwards from its right side. Those two moves, intro and apply, carry most proofs, and ∀ works exactly the same way.

The idea

intro h. If the goal is A → B, assume A, name the assumption h, and the goal becomes B. If the goal is ∀ x, P x, take an arbitrary x and the goal becomes P x. intro a b c does several at once.

apply h. If h : A → B and the goal is B, then it's enough to prove A: the goal becomes A. With h : ∀ n, P n → Q n and goal Q 0, Lean works out n = 0 itself.

Proofs of → are functions. A proof of A → B is literally a function turning proofs of A into proofs of B. So h a (apply h to a) is a proof of B, and exact hqr (hpq hp) does in one line what apply hqr, apply hpq, exact hp do in three.

Arrows associate to the right: p → q → r means p → (q → r), which is why intro hp hq can peel two at once.

Watch

Your turn

Check your understanding

The goal is p → q. What does intro hp do?

Adds hp : p above the line; the goal becomes q.
Proves p and stores it as hp.You don't prove p; you get to assume it.
Turns the goal into p.That is what apply does with a hypothesis p → q when the goal is q.

"To prove A implies B, assume A and prove B", written as one tactic.

With h : ∀ n, P n → Q n and goal Q 5, what is the goal after apply h?

P 5
∀ n, P nLean matches Q n with Q 5, so it only needs n = 5.
None: the goal is closed.Only if a proof of P 5 can be found automatically, which apply doesn't try.

You could also write exact h 5 hP if you had hP : P 5: h is a function of two arguments, a number and a proof.

Practice in the Lean editor

Swap the hypothesesTPIL Ch. 3 style

example (p q r : Prop) : (p → q → r) → (q → p → r) := by
  sorry

Solution

  intro h hq hp
  exact h hp hq

Write it yourselfTPIL Ch. 3 and 5

∧, ∨ and ↔

Each connective has a way to build it and a way to take it apart. Knowing which of the two you're doing tells you which tactic to reach for.

The idea

∧. Build: constructor (two goals) or exact ⟨ha, hb⟩. Take apart: obtain ⟨ha, hb⟩ := h, or use h.1 and h.2 directly.

∨. Build: left or right, choosing the side you can prove. Take apart: rcases h with ha | hb, which gives two goals, one for each case.

↔. Build: constructor gives the two implications. Use: h.mp (left to right) and h.mpr (right to left), or rw [h].

Patterns nest: obtain ⟨hp, hq | hr⟩ := h takes apart a p ∧ (q ∨ r) in one go. In a file, a · (typed \.) at the start of a line focuses on the next goal, which makes proofs with several goals easier to read; the practice problem below uses them.

Watch

Your turn

Check your understanding

The goal is p ∨ q and you have hq : q. What do you type?

right, then exact hq
left, then exact hqleft commits you to proving p.
constructorThat builds an ∧ or ↔ (both parts). An ∨ needs only one side, so you choose.

Or in one line: exact Or.inr hq.

You have h : p ∧ q and need q. Which works?

exact h.2
exact hh proves the pair, not its second half: a type mismatch.
rightright is for building an ∨ goal, not for using an ∧.

obtain ⟨hp, hq⟩ := h followed by exact hq also works, and is clearer when you need both halves.

Practice in the Lean editor

Associativity of ∨Nested cases and bullets

example (p q r : Prop) : (p ∨ q) ∨ r → p ∨ (q ∨ r) := by
  sorry

Hint

rcases h with (hp | hq) | hr gives three cases.

Solution

  intro h
  rcases h with (hp | hq) | hr
  · exact Or.inl hp
  · exact Or.inr (Or.inl hq)
  · exact Or.inr (Or.inr hr)

Write it yourselfTPIL Ch. 4 and 5

Equality and rw

Most of a computation in Lean is rewriting: replace one side of an equation with the other, then repeat. rw is literal and predictable, and when it fails its error tells you exactly why.

The idea

rw [h] with h : x = y replaces every x in the goal with y. rw [← h] replaces y with x. rw [h] at h2 rewrites the hypothesis h2 instead. After rewriting, rw tries rfl, so it often closes the goal by itself.

Lemmas are equations too. Nat.add_comm : ∀ n m, n + m = m + n and Nat.add_zero : ∀ n, n + 0 = n can be used in rw like hypotheses. Lean fills in n and m with the first match it finds; write Nat.add_comm a b to choose.

Literal matching. rw looks for the left-hand side exactly as written. 0 + (k + 1) does not contain 0 + k, even though it's "the same thing plus one"; you regroup first.

Watch

Your turn

Check your understanding

With h : x = y, what does rw [← h] do to the goal?

Replaces each y by x
Replaces each x by yThat's rw [h], left to right.
Proves y = xThat would be exact h.symm.

The arrow reverses the equation before rewriting.

rw fails with "Did not find an occurrence of the pattern". What does that mean?

The left-hand side of your equation doesn't appear, written exactly that way, in the goal.
The equation is false.Lean already knows it's true; it just can't find where to use it.
You need simp instead.Sometimes, but first check the goal: often a regrouping or an at h is missing.

In the induction module you'll see this with rw [ih] before the goal has been regrouped.

Practice in the Lean editor

Distribute and reorderThree library lemmas

example (a b c : Nat) : a * (b + c) = c * a + a * b := by
  sorry

Hint

Nat.mul_add, Nat.add_comm and Nat.mul_comm; give Nat.mul_comm its arguments so it hits the right product.

Solution

  rw [Nat.mul_add, Nat.add_comm, Nat.mul_comm c a]

Write it yourselfTPIL Ch. 4

∃: name a witness

To prove something exists, you say what it is and show it works. To use something that exists, you give it a name and carry on. That's all there is to ∃.

The idea

Build. refine ⟨w, ?_⟩ picks the witness w and leaves the proof that it works as a new goal (?_ marks the hole). exists w does the same and then tries simple tactics to finish. exact ⟨w, proof⟩ does both at once.

Use. obtain ⟨n, hn⟩ := h with h : ∃ n, P n gives you a fresh n and hn : P n. You don't get to choose n: it's whatever h promised.

The witness can depend on anything you already have: after intro n, n + 1 is a fine witness.

Watch

Your turn

Check your understanding

The goal is ∃ n : Nat, n * n = 9. What's the first step?

refine ⟨3, ?_⟩ (or exists 3)
obtain ⟨n, hn⟩ := …obtain is for using an ∃ you already have, not proving one.
intro nThat's for a ∀ or →. For ∃, you choose the number.

Then the goal is 3 * 3 = 9, which rfl or decide closes.

After obtain ⟨n, hn⟩ := h with h : ∃ n, n > 5, what do you know about n?

Only hn : n > 5
That n = 6Any number above 5 would do; Lean can't tell you which one h had in mind.
Nothing until you prove something about itYou get exactly the property h stated, as hn.

That's why the proof in the second exercise works for every such n, using omega on hn.

Practice in the Lean editor

From ∀ to ∃Any witness will do

example (P : Nat → Prop) (h : ∀ n, P n) : ∃ n, P n := by
  sorry

Solution

  exact ⟨0, h 0⟩

Drop half a propertyA pattern inside a pattern

example (P Q : Nat → Prop) : (∃ n, P n ∧ Q n) → ∃ n, P n := by
  sorry

Solution

  intro h
  obtain ⟨n, hp, _⟩ := h
  exact ⟨n, hp⟩

The underscore throws away the part you don't need.

Write it yourselfTPIL Ch. 3

¬ and False

Negation looks special but isn't: ¬p is defined to mean p → False. So you prove it with intro, and use it by applying it, exactly like any implication.

The idea

Prove ¬p: intro hp, then reach False.

Use hnp : ¬p: if you have hp : p, then hnp hp : False. If the goal is False, exact hnp hp; or apply hnp to turn the goal False into p.

Impossible arithmetic. A hypothesis like h : n + 1 = 0 about natural numbers is itself a contradiction; omega sees it, and so does the library lemma Nat.succ_ne_zero.

Proofs by contradiction of the form "assume not p, derive False, conclude p" need classical logic (Classical.byContradiction, or by_contra in Mathlib). The exercises here don't: they are the constructive half of TPIL Chapter 3.

Watch

Your turn

Check your understanding

What is ¬p by definition?

p → False
p = FalsePropositions aren't compared with = to define negation; it's an implication.
A separate primitive that needs its own tacticsNo special tactics: intro and function application handle it.

That's why intro hp hnp works on the goal p → ¬¬p: the goal is really p → (¬p → False).

The goal is False, and you have hp : p and hnp : ¬p. What closes it?

exact hnp hp
exact hp hnphp is a proof, not a function; it's hnp that takes an argument.
rflFalse isn't an equation.

contradiction also works here: it looks for a hypothesis and its negation.

Practice in the Lean editor

One of De Morgan's lawsTPIL Ch. 3 exercise list

example (p q : Prop) : ¬(p ∨ q) → ¬p ∧ ¬q := by
  sorry

Solution

  intro h
  constructor
  · intro hp
    exact h (Or.inl hp)
  · intro hq
    exact h (Or.inr hq)

Write it yourselfTPIL Ch. 7 and 8

Induction and recursion

A natural number is either 0 or one more than a natural number, and Lean defines Nat exactly that way. Induction is the matching proof technique, and recursive definitions unfold one step at a time inside it.

The idea

induction n replaces a goal about n by two goals: zero (the statement for 0) and succ (for k + 1, assuming it for k). Lean gives the new variable and hypothesis inaccessible names, shown with ✝, until you name them.

case succ k ih => focuses on the step case and names the variable k and the induction hypothesis ih. The tactics for that case go on the following lines, indented. case zero => rfl handles a one-line case.

Recursive definitions. A definition by pattern matching, like double (n + 1) = double n + 2, can be used as a rewrite rule: rw [double] unfolds one step of it.

Which arithmetic tactic. omega proves anything true in linear arithmetic over Nat and Int (sums, constants, inequalities), but treats a product of two variables as unknown. grind also normalizes polynomial identities such as the last step of Gauss's sum.

Watch

Your turn

Check your understanding

Right after induction n, you type rw [ih]. Lean says Unknown identifier `ih`. Why?

The hypothesis exists, but it has an inaccessible name until you name it with case succ k ih =>.
Induction didn't produce a hypothesis.It did; look at the succ goal: a✝ : ….
rw can't use hypotheses.It can; the problem is the name.

The ✝ marks names Lean made up and won't let you type. This is one of the most common confusions when reading Lean proofs. The error is real: try it in the worked example's exercise.

Why can't omega prove k * (k + 1) + 2 * (k + 1) = (k + 1) * (k + 1 + 1)?

It's nonlinear: omega treats k * k as an unknown, and the identity needs algebra.
It's false.Expand both sides: each is k² + 3k + 2.
omega only works on Int.It handles Nat too.

With Mathlib, ring is the usual tool. In plain Lean, grind does it, as the third exercise shows.

Practice in the Lean editor

Powers of two are positiveUnfold, then arithmetic

def pow2 : Nat → Nat
  | 0 => 1
  | n + 1 => 2 * pow2 n

example (n : Nat) : 0 < pow2 n := by
  sorry

Solution

  induction n
  case zero => decide
  case succ k ih =>
    rw [pow2]
    omega

Length of an appendInduction on a list

example (xs ys : List Nat) : (xs ++ ys).length = xs.length + ys.length := by
  sorry

Hint

Lists are built from nil and cons x xs, so induction xs gives cases nil and cons; name the parts with case cons x xs ih =>.

Solution

  induction xs
  case nil => simp
  case cons x xs ih =>
    simp [ih]
    omega

(The library already has this as List.length_append, so simp alone also works.)

Write it yourselfTPIL Ch. 5

Automation, and reading errors

Real proofs lean on tactics that do a lot at once. Knowing what each one can do, and reading the error when it can't, is what makes other people's proofs readable.

The idea

simp rewrites with a large set of simplification lemmas, like xs ++ [] = xs and n + 0 = n, until nothing changes. simp [h] adds your own equations. "simp made no progress" means no rule applied.

omega decides linear arithmetic over Nat and Int, including hypotheses. decide evaluates a statement about concrete values. grind combines rewriting, case analysis and algebra.

exact? searches the library for a lemma that closes the goal and suggests it: on a + b = b + a it prints Try this: exact Nat.add_comm a b. It is how you find names like Nat.add_comm in the first place.

Reading an error. Lean's errors say what it expected and what it got. Type mismatch: you gave a proof of something else. Unknown identifier: that name doesn't exist here (not yet introduced, or misspelled). unknown tactic: not in plain Lean (linarith, ring, norm_num are from Mathlib). unsolved goals: the proof ended with goals left.

Your turn

Check your understanding

Each error below is a real Lean message from an exercise on this page.

The goal is p → q → p. Someone types exact hp and Lean says: Unknown identifier `hp`. What went wrong?

Nothing called hp exists yet: intro hp has to come first.
hp is spelled wrong.Possible in general, but here no hypothesis exists at all: the goal view has only p q : Prop.
exact is the wrong tactic for implications.exact works with any proof; the problem is the name.

Before reading the error, read the goal view: names you can use are exactly the ones above the ⊢.

The goal is 2 + 3 = 5. Someone types exact 5. Lean says: numerals are data in Lean, but the expected type is a proposition. What does that mean?

exact needs a proof of the goal, and 5 is a number, not a proof.
The goal is false.It's true; rfl proves it.
Lean can't add numbers.It can: that's what rfl and decide rely on.

This is the "proofs are objects with types" idea from module 1 from the other side: the goal is a type, and only a proof of it fits.

Someone types linarith and Lean says unknown tactic, though they saw it in a textbook proof. Why?

It comes from Mathlib, which isn't loaded.
It was removed from Lean.It was never part of core Lean.
It's spelled linear_arith.The name is right; the library is missing.

Most proofs you read online use Mathlib (import Mathlib at the top). In plain Lean, omega covers what linarith does over the naturals and integers.

Practice in the Lean editor

Tactics are optionalThe same proof as a term

The worked example in module 2 can be written with no tactics at all, as a function. Fill in the term.

example (p q r : Prop) : (p → q) → (q → r) → p → r :=
  sorry

Solution

  fun hpq hqr hp => hqr (hpq hp)

A proof of an implication is a function, so this is literally the proof. Reading terms like this is the other half of reading Lean (TPIL Ch. 3).

Ask the libraryexact? finds lemma names

example (a b : Nat) : a + b = b + a := by
  exact?

What Lean says

Try this: exact Nat.add_comm a b. Click the suggestion in the editor to replace exact? with it.