Tactics

Chapter 1 represented proofs directly as terms. Longer arguments are usually written as tactic scripts: sequences of commands that construct proof terms. The keyword by begins a tactic script.

Tactics operate on the goal state, which lists the current hypotheses and the conclusion still to prove. Each tactic transforms this state or closes a goal. In the playground, placing the cursor after a tactic displays the state at that point.

y1 y0 : Fin 3 → ℝ
h : ∀ i, y0 i ≤ y1 i
⊢ y0 0 ≤ y1 0

The hypotheses appear above the turnstile ⊢; the target appears below it. A proof is complete when no goals remain.

intro and exact

theorem effect_nonneg_at_zero (y1 y0 : Fin 3 → ℝ) :
    (∀ i, y0 i ≤ y1 i) → y0 0 ≤ y1 0 := by
  intro h
  exact h 0

intro h moves the antecedent of an →, or the bound variable of a ∀, out of the goal and into the hypotheses. It is the tactic spelling of fun h => …. exact e closes the goal with the term e, which must have exactly the goal’s type. The proof above is one of each, starting from

y1 y0 : Fin 3 → ℝ
⊢ (∀ (i : Fin 3), y0 i ≤ y1 i) → y0 0 ≤ y1 0

1. intro h

   The target is an implication, so its antecedent can be assumed: intro h names it h and removes it from the target. What is left to prove is the conclusion alone, the inequality at unit 0.

   Goal

   y1 y0 : Fin 3 → ℝ
   h : ∀ (i : Fin 3), y0 i ≤ y1 i
   ⊢ y0 0 ≤ y1 0

2. exact h 0

   h is a proof of a ∀, which chapter 1 established is a function, so h 0 is its instance at unit 0 — a proof of y0 0 ≤ y1 0. That is the goal character for character, so exact accepts it and no goals remain.

That pair is the floor. Everything else is a way of getting a goal into a shape where exact applies.

Working backwards: apply and refine

theorem obs_le_of_le (a b c : ℝ) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by
  apply le_trans
  · exact hab
  · exact hbc

theorem mean_bounds (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a ∧ 0 ≤ a + b := by
  refine ⟨ha, ?_⟩
  exact add_nonneg ha hb

apply f unifies the conclusion of f with the goal and leaves you owing f’s hypotheses. With le_trans : a ≤ b → b ≤ c → a ≤ c and the goal a ≤ c, one goal becomes two, and the intermediate b is a metavariable that later steps will pin down:

case a
a b c : ℝ
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ ?b

case a
a b c : ℝ
hab : a ≤ b
hbc : b ≤ c
⊢ ?b ≤ c

case b
a b c : ℝ
hab : a ≤ b
hbc : b ≤ c
⊢ ℝ

Three goals, not two, and the third is the surprise: ?b is an unknown real number, so Lean owes itself a term of type ℝ as well as the two inequalities. You never have to supply it — exact hab forces ?b := b by unification and the third goal disappears with it — but seeing it once explains why apply sometimes leaves a goal that is a type rather than a proposition. When that is a nuisance, exact le_trans hab hbc or refine le_trans ?_ hbc pins the intermediate down from the start.

The · bullets in the script focus one goal at a time. They are not decoration: they scope the tactics inside them, so a proof stays readable and a change to one branch cannot silently leak into the other.

1. apply le_trans

   le_trans : a ≤ b → b ≤ c → a ≤ c. Its conclusion unifies with the goal a ≤ c — fixing the lemma’s a and c, and leaving its b open — so what remains is the lemma’s two hypotheses, plus the metavariable ?b displayed above.

2. · exact hab

   The bullet focuses the first of those goals, a ≤ ?b. Supplying hab : a ≤ b closes it and, by unification, decides ?b := b; the goal that asked for a real number is answered by the same act, which is why the script never mentions it.

3. · exact hbc

   With ?b now known to be b, the second goal reads b ≤ c, which is hbc. Reading the script backwards: we claimed the conclusion follows by transitivity, and then paid the two debts transitivity incurs.

refine is exact with holes. You write the shape of the answer and put ?_ where you want a new goal, which is how the second theorem gets from a conjunction to the one inequality it has to work for.

1. refine ⟨ha, ?_⟩

   The goal 0 ≤ a ∧ 0 ≤ a + b is a pair, so a proof of it is a pair. The left component is ha outright; ?_ in the right slot says “leave that one to me”, and it becomes the goal shown below.

   Goal

   a b : ℝ
   ha : 0 ≤ a
   hb : 0 ≤ b
   ⊢ 0 ≤ a + b

2. exact add_nonneg ha hb

   add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b is the fact that a sum of non-negatives is non-negative. Fed the two hypotheses in order, it has exactly the type of the remaining goal.

This is the tactic to reach for when you know the structure of the argument and not yet the details, which — in a formalization of something you already understand — is most of the time.

Rewriting

theorem obs_of_treated (y1 yobs : ℝ) (h : yobs = y1) (hy : y1 = 3) : yobs = 3 := by
  rw [h]
  exact hy

theorem obs_of_treated' (y1 yobs : ℝ) (h : yobs = y1) (hy : y1 = 3) : yobs = 3 := by
  rw [← hy]
  exact h

theorem effect_at_unit (y1 y0 : Fin 3 → ℝ) (c : ℝ)
    (h : ∀ i, y1 i - y0 i = c) (hc : c = 2) : y1 1 - y0 1 = 2 := by
  have h1 := h 1
  rw [hc] at h1
  exact h1

rw [h] where h : a = b replaces every occurrence of a in the goal by b. It is the workhorse: a statistical identity is a chain of substitutions, and rw is substitution.

obs_of_treated is two lines: turn the observed outcome into the treated potential outcome, then quote the value of that.

1. rw [h]

   h : yobs = y1 reads left to right, so every yobs in the goal yobs = 3 becomes y1. Statistically this is the substitution “the unit was treated, so what we observed is its treated potential outcome”.

   Goal

   y1 yobs : ℝ
   h : yobs = y1
   hy : y1 = 3
   ⊢ y1 = 3

2. exact hy

   The goal is now y1 = 3, which is the hypothesis hy.

Three features of rw are used throughout the book.

It goes left to right, and ← reverses it. obs_of_treated' proves the same theorem from the other end.

1. rw [← hy]

   hy : y1 = 3 used forwards would look for a y1 in the goal yobs = 3 and find none. The arrow reverses it, so the 3 in the goal becomes y1 instead and the goal turns into the hypothesis h.

   Goal

   y1 yobs : ℝ
   h : yobs = y1
   hy : y1 = 3
   ⊢ yobs = y1

2. exact h

   h : yobs = y1 is now the goal exactly. Choosing the direction is most of the skill; a rewrite that “does not apply” is usually the right lemma facing the wrong way.

It rewrites the goal unless you say otherwise. rw [hc] at h1 rewrites inside the hypothesis h1. effect_at_unit uses both that and a have to work on the assumption rather than on the target.

1. have h1 := h 1

   h is the constant-effects assumption, one equation per unit; h 1 is its instance at unit 1, and have gives that instance a name. Note the form: have name := term with no stated type, because the type is whatever the term has — here y1 1 - y0 1 = c.

   Goal

   y1 y0 : Fin 3 → ℝ
   c : ℝ
   h : ∀ (i : Fin 3), y1 i - y0 i = c
   hc : c = 2
   h1 : y1 1 - y0 1 = c
   ⊢ y1 1 - y0 1 = 2

2. rw [hc] at h1

   hc : c = 2 rewritten in h1 replaces the constant by its value, so h1 becomes y1 1 - y0 1 = 2. Nothing has happened to the goal; the point of at is that the hypothesis, not the target, was the thing in the wrong shape.

3. exact h1

   h1 is now literally the goal. Two lines of massaging a hypothesis, one line to hand it over — a shape you will write hundreds of times.

It closes the goal if the result is rfl. After a successful rewrite Lean tries rfl, which is why many rw chains end without an explicit exact. This is convenient and occasionally confusing: a rw that “does too much” has usually just finished.

simp and simp only

theorem sum_two_outcomes (y : Fin 3 → ℝ) : y 0 + 0 + (y 1 * 1) = y 0 + y 1 := by
  simp only [add_zero, mul_one]

theorem cleanup_hypothesis (x : ℝ) (h : x + 0 = 5) : x = 5 := by
  simp only [add_zero] at h
  exact h

simp rewrites with the entire @[simp] database until nothing changes. It is enormously useful and completely opaque: you cannot tell from the script what was used, and a Mathlib update can change the answer.

simp only [add_zero, mul_one] uses exactly the lemmas named. In anything someone else will read — a tutorial, a paper artefact, a library — prefer simp only. The way to get the list is to write simp?, read the simp only [...] it prints, and paste that in. simp at h normalizes a hypothesis instead of the goal, and simp_all does both everywhere, which is powerful and the least readable option of all.

Both theorems in the block are one simp only, and the list is short enough to read lemma by lemma.

1. simp only [add_zero, mul_one]

   In sum_two_outcomes the two named lemmas do one job each. add_zero (a + 0 = a) deletes the + 0, leaving the goal shown below; mul_one (a * 1 = a) then deletes the * 1, after which the two sides are the same term and simp only closes the goal itself. Neither lemma knows anything about outcomes — this is bookkeeping, and the reason to name the lemmas is so that a reader can see that nothing but bookkeeping happened.

   Goal

   y : Fin 3 → ℝ
   ⊢ y 0 + y 1 * 1 = y 0 + y 1

2. simp only [add_zero] at h

   cleanup_hypothesis has the clutter in the hypothesis instead, so at h points the same rewrite there: h : x + 0 = 5 becomes h : x = 5. The goal is untouched.

   Goal

   x : ℝ
   h : x = 5
   ⊢ x = 5

3. exact h

   Which is now the goal. Compare this with rw [add_zero] at h: the same effect here, but simp only keeps going until nothing in its list applies, so it survives a hypothesis with three stray + 0s where rw would need three rewrites.

Building and taking apart

theorem both_nonneg (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a ∧ 0 ≤ b := by
  constructor
  · exact ha
  · exact hb

theorem exists_positive_effect (y1 y0 : Fin 3 → ℝ) (h : y0 2 < y1 2) :
    ∃ i, y0 i < y1 i := by
  use 2

constructor applies the constructor of an inductive goal. On p ∧ q it splits one goal into two:

case left
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a

case right
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ b

1. constructor

   The goal is a conjunction, and And has one constructor taking one proof per side, so constructor applies it and asks for both. The two goals above are the arguments it now needs.

2. · exact ha

   The first bullet answers 0 ≤ a, which is the hypothesis ha.

3. · exact hb

   The second answers 0 ≤ b with hb. This proof is refine ⟨ha, hb⟩ written in three lines instead of one; constructor earns its keep when the two halves are long enough that you want them separated.

use w supplies the witness for an ∃ goal and leaves the property. It also tries rfl and the hypotheses afterwards, which is why use 2 finishes exists_positive_effect outright: after substituting the witness the remaining goal y0 2 < y1 2 is literally the hypothesis h. When use does not close the goal, you are left with the property to prove, which is what you wanted.

theorem exists_of_exists (y1 y0 : Fin 3 → ℝ) (h : ∃ i, y1 i - y0 i = 2) :
    ∃ i, 0 < y1 i - y0 i := by
  obtain ⟨i, hi⟩ := h
  exact ⟨i, by rw [hi]; norm_num⟩

theorem obs_nonneg (yobs y1 y0 : ℝ) (h1 : 0 ≤ y1) (h0 : 0 ≤ y0)
    (h : yobs = y1 ∨ yobs = y0) : 0 ≤ yobs := by
  rcases h with h | h
  · rw [h]; exact h1
  · rw [h]; exact h0

Going the other way, obtain ⟨i, hi⟩ := h destructs an ∃ or an ∧ in a hypothesis:

y1 y0 : Fin 3 → ℝ
i : Fin 3
hi : y1 i - y0 i = 2
⊢ ∃ i, 0 < y1 i - y0 i

Note what the witness i is and is not: it is a genuine unit of the population, opaque except for hi. The rest of the proof has to produce a new existential out of it.

1. obtain ⟨i, hi⟩ := h

   Destruct the hypothesis. i is the unit the hypothesis promised and hi its property, and the hypothesis h itself is gone — its content is now in those two names. The goal, shown above, is unchanged.

2. exact ⟨i, …⟩

   The goal is an ∃, so the anonymous constructor from chapter 1 builds it: the same unit i as the witness, and then a proof that it works.

   Goal

   y1 y0 : Fin 3 → ℝ
   i : Fin 3
   hi : y1 i - y0 i = 2
   ⊢ 0 < y1 i - y0 i

3. rw [hi]

   Inside the bracket, tactic mode again. hi says the effect at i equals 2, so rewriting turns the goal 0 < y1 i - y0 i into arithmetic on numerals.

   Goal

   y1 y0 : Fin 3 → ℝ
   i : Fin 3
   hi : y1 i - y0 i = 2
   ⊢ 0 < 2

4. norm_num

   0 < 2, which norm_num decides. The whole proof is “the unit that has effect exactly two is a unit that has positive effect”, and each of the four steps is one clause of that sentence.

rcases h with ⟨i, hi⟩ is the same tactic spelled differently, and cases h with | intro i hi => … is the low-level version. Use obtain for conjunctions and existentials, and rcases h with h | h for a disjunction, where the | produces one goal per side:

case inl
yobs y1 y0 : ℝ
h1 : 0 ≤ y1
h0 : 0 ≤ y0
h : yobs = y1
⊢ 0 ≤ yobs

case inr
yobs y1 y0 : ℝ
h1 : 0 ≤ y1
h0 : 0 ≤ y0
h : yobs = y0
⊢ 0 ≤ yobs

1. rcases h with h | h

   One goal per disjunct, each with the corresponding equation available under the same name h — reusing the name is idiomatic when the two branches are symmetric. The two states above are what rcases produced.

2. · rw [h]; exact h1

   In the first branch h : yobs = y1, so rewriting the goal 0 ≤ yobs gives the goal shown below, which is the hypothesis h1. The ; is sequencing inside one bullet, nothing more.

   Goal

   yobs y1 y0 : ℝ
   h1 : 0 ≤ y1
   h0 : 0 ≤ y0
   h : yobs = y1
   ⊢ 0 ≤ y1

3. · rw [h]; exact h0

   The second branch is the same two tactics with y0 in place of y1. This is the whole of design-based reasoning about an observed outcome: it is one of the two potential outcomes, you do not know which, so you argue twice.

That two-case shape is the treated/control split, and you will meet it in every argument about an indicator.

Structuring a proof: have, show, calc

theorem variance_shortcut (x m : ℝ) : (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2 := by
  have expand : (x - m) ^ 2 = (x - m) * (x - m) := sq (x - m) ▸ rfl
  show (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2
  rw [expand]
  ring

have name : statement := proof proves an intermediate fact and adds it to the context. It is the Lean spelling of “note that”, and it is the main tool for making a proof readable: state the intermediate quantity, then use it.

show restates the goal in a definitionally equal form. It changes nothing that Lean can see and everything a reader can: it says, at this point in the argument, what you believe you are proving. Use it after a chain of unfoldings.

variance_shortcut is $(x-m{)}^2=x^2-2mx+m^2$, the expansion every variance calculation begins with. It is a ring identity, and this proof takes the long way round on purpose, to show the two structuring tactics in a proof small enough to hold in your head.

1. have expand : (x - m) ^ 2 = (x - m) * (x - m) := sq (x - m) ▸ rfl

   The intermediate fact is “a square is a product with itself”. Its proof is a term: sq is the Mathlib lemma a ^ 2 = a * a, so sq (x - m) is that equation at a := x - m, and e ▸ rfl rewrites the goal with e and then closes what is left by reflexivity — here the goal becomes (x - m) * (x - m) = (x - m) * (x - m), which rfl proves. Writing the proof as := sq (x - m) on its own would have done the same job more plainly, since that term already has the stated type. Either way the goal is untouched and the context has gained expand.

   Goal

   x m : ℝ
   expand : (x - m) ^ 2 = (x - m) * (x - m)
   ⊢ (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2

2. show (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2

   This restates the goal as itself. Nothing changes, and that is the point of including it here: show is a claim about what you think the goal is, so it is free to write and it fails loudly when you are wrong. In a proof that had just unfolded three definitions it would be the most useful line in the script; in this one it is a placeholder for that habit.

3. rw [expand]

   Now expand is used: rewriting with it left to right turns the (x - m) ^ 2 in the goal into (x - m) * (x - m).

   Goal

   x m : ℝ
   expand : (x - m) ^ 2 = (x - m) * (x - m)
   ⊢ (x - m) * (x - m) = x ^ 2 - 2 * m * x + m ^ 2

4. ring

   Multiply out and compare normal forms. ring would have closed the original goal in one line — squares are part of its normal form — so expand bought nothing mathematically. What the script demonstrates is the shape: name the intermediate step, restate the target, rewrite, close.

theorem obs_decomposition (z y1 y0 : ℝ) :
    z * y1 + (1 - z) * y0 = y0 + z * (y1 - y0) := by
  calc z * y1 + (1 - z) * y0
      = z * y1 + y0 - z * y0 := by ring
    _ = y0 + (z * y1 - z * y0) := by ring
    _ = y0 + z * (y1 - y0) := by rw [mul_sub]

calc writes a chain of equalities or inequalities in the usual mathematical form, with the justification for each step to the right of :=, and each _ standing for the previous right-hand side. The example is the decomposition that every discussion of potential outcomes starts from.

Claim. For any treatment indicator $z$ and any pair of potential outcomes, $z{y}_1+(1-z)y_0=y_0+z(y_1-y_0)$.

Read that back and the three calc steps are the three sentences.

1. = z * y1 + y0 - z * y0 := by ring

   Distribute $(1-z)y_0$. Each step of a calc is its own goal — the one shown below — and by ring closes this one because it is a polynomial identity.

   Goal

   ⊢ z * y1 + (1 - z) * y0 = z * y1 + y0 - z * y0

2. _ = y0 + (z * y1 - z * y0) := by ring

   Rearrange so that the control outcome is out front and the two $z$ terms are together. The _ is the previous right-hand side, so this step’s goal is the one shown, and again it is pure rearrangement. The step exists because the next one is a rewrite, and a rewrite only fires on the syntax in front of it: the z * y1 - z * y0 has to be sitting in one bracket before mul_sub can recognize it.

   Goal

   ⊢ z * y1 + y0 - z * y0 = y0 + (z * y1 - z * y0)

3. _ = y0 + z * (y1 - y0) := by rw [mul_sub]

   mul_sub : a * (b - c) = a * b - a * c. Rewriting left to right turns the z * (y1 - y0) on the right of this step’s equation into z * y1 - z * y0, which makes both sides identical, and rw closes a goal that has become rfl. by ring would also have worked; doing it by hand shows where the factoring happens, which in the variance calculations of chapter 9 is the step that matters.

A calc block can mix = and ≤, so a variance bound reads as a chain of inequalities rather than as a pile of rewrites. Where you have a choice, choose calc.

The automation

A handful of tactics do the arithmetic so you do not have to. Knowing which one to reach for is most of the practical skill of writing Lean.

theorem square_of_deviation (x m : ℝ) :
    (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2 := by ring

theorem indicator_algebra (z y1 y0 : ℝ) :
    z * y1 + (1 - z) * y0 = y0 + z * (y1 - y0) := by ring

ring proves any identity that holds in every commutative ring: it normalizes both sides and compares. Every “expand the square” step in a variance calculation is a ring call, and ring treats division as multiplication by an inverse, so it does not need to know that a denominator is nonzero — it also cannot use that fact if you have it.

ring knows nothing about hypotheses and nothing about inequalities. If your goal needs either, you want the next two.

theorem mean_between (a b : ℝ) (hab : a ≤ b) : a ≤ (a + b) / 2 := by linarith

theorem two_mul_le_sq_add_sq (a b : ℝ) : 2 * (a * b) ≤ a ^ 2 + b ^ 2 := by
  nlinarith [sq_nonneg (a - b)]

linarith closes any goal that follows from the hypotheses by adding inequalities and scaling them by positive constants — linear arithmetic over an ordered field. It looks at every hypothesis in context, so the usual way to use it is to have the facts you need and then call it.

nlinarith is linarith plus products of hypotheses and squares. The idiom nlinarith [sq_nonneg (a - b)] — hand it the square you know is non-negative — is how most Cauchy–Schwarz-flavoured bounds get closed.

theorem variance_denominator_pos (n : ℕ) (hn : 0 < n) : 0 < (n : ℝ) ^ 2 + 1 := by
  positivity

theorem mean_eq_iff (a b m : ℝ) (h : (a + b) / 2 = m) : a + b = 2 * m := by
  field_simp at h
  linarith

positivity proves 0 < e, 0 ≤ e or e ≠ 0 by walking the syntax of e: sums of squares, sample sizes, products of positives. It is the right tactic for the side conditions that field_simp and div_pos demand.

field_simp clears denominators, given that they do not vanish. It looks for the nonvanishing facts in context, which is why proofs about means begin with a line like have hn : (n : ℝ) ≠ 0 := …. Afterwards the goal is polynomial, so field_simp is almost always followed by ring or linarith.

variance_denominator_pos is one positivity call: the expression $n^2+1$ is a square plus a positive constant, and walking that syntax is exactly what the tactic does — the hypothesis 0 < n is not even needed. mean_eq_iff is the two-line pattern.

1. field_simp at h

   The hypothesis is (a + b) / 2 = m. Multiplying through by the denominator turns it into a + b = 2 * m; the 2 needs no side condition, since field_simp can see for itself that it is not zero. Note that this rewrote the hypothesis, and that what came out happens to be the goal.

   Goal

   a b m : ℝ
   h : a + b = 2 * m
   ⊢ a + b = 2 * m

2. linarith

   The goal is now a linear consequence of h — in fact it is h — so linarith closes it, and exact h would too. Writing linarith is the robust choice: field_simp decides for itself how to arrange a product, so the hypothesis it leaves may be a + b = 2 * m or a + b = m * 2 depending on the version, and a tactic that does linear arithmetic does not care which.

theorem concrete_mean : ((2 : ℝ) + 4 + 6) / 3 = 4 := by norm_num

theorem control_count (n n₁ : ℕ) (h : n₁ ≤ n) : n₁ + (n - n₁) = n := by omega

theorem all_units_small : ∀ i : Fin 3, i.val < 3 := by decide

norm_num evaluates concrete numerals in ℕ, ℤ, ℚ or ℝ, and extends simp with numeric lemmas.

omega is a decision procedure for linear arithmetic over ℕ and ℤ, including the truncated subtraction that makes ℕ treacherous. Sample sizes and group counts live in ℕ, so omega comes up constantly: n₁ + (n - n₁) = n given n₁ ≤ n is an omega goal and nothing else will do it cleanly.

decide evaluates a decidable proposition. It works only when everything is concrete and small, and — the part that matters for reading other people’s work — it proves the claim for that instance only.

theorem cast_add (n₁ n₀ : ℕ) : ((n₁ + n₀ : ℕ) : ℝ) = (n₁ : ℝ) + (n₀ : ℝ) := by
  push_cast
  ring

theorem cast_sub (n k : ℕ) (h : k ≤ n) : ((n - k : ℕ) : ℝ) = (n : ℝ) - (k : ℝ) := by
  rw [Nat.cast_sub h]

push_cast pushes coercions towards the leaves of an expression; norm_cast tries to eliminate them. Chapter 3 does casts properly. The one thing to carry away now is the second example: no cast tactic will move a cast through a ℕ-subtraction for you, because ((n - k : ℕ) : ℝ) = (n : ℝ) - k is false without k ≤ n; the proof has to hand Nat.cast_sub the hypothesis h explicitly. When a cast tactic makes no progress, suspect the statement before the tactic.

1. push_cast

   In cast_add the cast sits outside a sum of naturals. push_cast moves it inward, so ↑(n₁ + n₀) becomes ↑n₁ + ↑n₀ and both sides of the goal are the same sum of two casts.

   Goal

   n₁ n₀ : ℕ
   ⊢ ↑n₁ + ↑n₀ = ↑n₁ + ↑n₀

2. ring

   Closes what is left. rfl would also do it — after the cast has been pushed the two sides are the same term — and ring is the habit worth having, because in a real proof push_cast leaves an expression that is equal to the target rather than identical to it.

3. rw [Nat.cast_sub h]

   cast_sub is the theorem the tactics cannot do for you. Nat.cast_sub : k ≤ n → ↑(n - k) = ↑n - ↑k takes the inequality as an argument, so Nat.cast_sub h is the equation specialized to this h, and one rewrite turns the left side of the goal into the right and closes it by reflexivity.

Case splits and contradictions

theorem indicator_sq (i : Fin 3) (z : Finset (Fin 3)) :
    (if i ∈ z then (1 : ℝ) else 0) * (if i ∈ z then (1 : ℝ) else 0)
      = if i ∈ z then (1 : ℝ) else 0 := by
  by_cases h : i ∈ z
  · rw [ite_eq_left h, mul_one]
  · rw [ite_eq_right h, mul_zero]

by_cases h : p splits into the case where p holds and the case where it does not. It works for any proposition: if p has a Decidable instance Lean uses it, and otherwise it falls back on Classical.em. For an indicator this is the entire story — Z i is 1 on the treated and 0 on the controls — so every fact about an indicator is two computations:

case pos
i : Fin 3
z : Finset (Fin 3)
h : i ∈ z
⊢ ((if i ∈ z then 1 else 0) * if i ∈ z then 1 else 0) = if i ∈ z then 1 else 0

case neg
i : Fin 3
z : Finset (Fin 3)
h : i ∉ z
⊢ ((if i ∈ z then 1 else 0) * if i ∈ z then 1 else 0) = if i ∈ z then 1 else 0

Note that the goal is unchanged in both branches: by_cases adds a hypothesis and nothing else. The work is done afterwards.

1. by_cases h : i ∈ z

   Two goals, differing only in the hypothesis h : i ∈ z or h : i ∉ z. Both targets are still the full statement about the if, as the two states above show.

2. · rw [ite_eq_left h, mul_one]

   ite_eq_left h : (if c then t else e) = t given a proof of c. Rewriting with it replaces all three ifs in the goal by their left branch 1, leaving 1 * 1 = 1; then mul_one turns the left side into 1 and the goal closes by reflexivity.

   Goal

   i : Fin 3
   z : Finset (Fin 3)
   h : i ∈ z
   ⊢ 1 * 1 = 1

3. · rw [ite_eq_right h, mul_zero]

   The mirror: ite_eq_right h takes a proof of ¬ c and collapses the if to its right branch 0, leaving 0 * 0 = 0, and mul_zero finishes. Two branches, four rewrites, and no arithmetic — which is what “an indicator is algebra with two cases” looks like when written out.

theorem from_absurd_hypotheses (n : ℕ) (h1 : 0 < n) (h2 : n = 0) : (1 : ℝ) = 2 := by
  exfalso
  rw [h2] at h1
  exact absurd h1 (lt_irrefl 0)

theorem from_absurd_hypotheses' (n : ℕ) (h1 : 0 < n) (h2 : n = 0) : (1 : ℝ) = 2 := by
  subst h2
  contradiction

theorem nonneg_of_not_neg (x : ℝ) (h : ¬ (x < 0)) : 0 ≤ x := by
  by_contra hc
  exact h (lt_of_not_ge hc)

exfalso replaces any goal by False; contradiction finds an outright inconsistency in the context and closes the goal; by_contra h assumes the negation of the goal and asks you for False.

The first two theorems are the same worthless theorem proved two ways, and the third is the honest use of the same machinery.

1. exfalso

   Anything follows from False, so a proof of False is a proof of 1 = 2. This throws the conclusion away — and notice that the conclusion was never looked at, which is the whole complaint about theorems like this one.

   Goal

   n : ℕ
   h1 : 0 < n
   h2 : n = 0
   ⊢ False

2. rw [h2] at h1

   h2 : n = 0 rewritten in h1 : 0 < n gives h1 : 0 < 0. The two hypotheses have been brought into the same expression, which is where a contradiction becomes visible.

   Goal

   n : ℕ
   h1 : 0 < 0
   h2 : n = 0
   ⊢ False

3. exact absurd h1 (lt_irrefl 0)

   absurd : p → ¬ p → q with p := (0 < 0): h1 is the proof, lt_irrefl 0 is the refutation, and q is the False we owe.

from_absurd_hypotheses' does it in two lines instead of three.

1. subst h2

   subst eliminates a variable that a hypothesis equates to something: h2 says n is 0, so n is replaced by 0 everywhere and both n and h2 disappear from the context. What is left is h1 : 0 < 0 and the untouched goal.

   Goal

   h1 : 0 < 0
   ⊢ 1 = 2

2. contradiction

   contradiction scans the context for a hypothesis that cannot hold — here 0 < 0, which is impossible on the naturals by the definition of < — and closes any goal when it finds one. It needs no exfalso, because it is not proving the goal, it is discharging the context.

nonneg_of_not_neg is the one to imitate. It proves something true, and it uses the negation because ¬ (x < 0) and 0 ≤ x are the same fact stated on opposite sides of a ¬.

1. by_contra hc

   The goal 0 ≤ x is replaced by False, with its negation hc : ¬ (0 ≤ x) added to the context. On a linear order this is the classical step, and it is where the argument gets its leverage: the hypothesis and the assumed negation are now both statements about the sign of x.

   Goal

   x : ℝ
   h : ¬x < 0
   hc : ¬0 ≤ x
   ⊢ False

2. exact h (lt_of_not_ge hc)

   lt_of_not_ge : ¬ (b ≤ a) → a < b turns hc into a proof of x < 0. And h is ¬ (x < 0), which is (x < 0) → False, so applying h to that proof produces the False we owe. Nothing here is specific to ℝ; it is the ¬ ¬ p → p step of chapter 1’s stretch exercise, done by by_contra.

Then read the first two theorems again. Both prove (1 : ℝ) = 2 from 0 < n and n = 0, and in neither is the “conclusion” ever touched. A theorem whose hypotheses cannot all hold is provable and worthless, and no compiler will warn you, because there is nothing wrong. This is the failure mode chapter 5 gives you a checklist for, and it is the reason the last section of this chapter exists.

Extensionality

theorem outcomes_eq (y1 y0 : Fin 3 → ℝ) (h : ∀ i, y1 i = y0 i) : y1 = y0 := by
  funext i
  exact h i

theorem assignments_eq (s t : Finset (Fin 3)) (h : ∀ i, i ∈ s ↔ i ∈ t) : s = t := by
  ext i
  exact h i

Two outcome vectors are equal exactly when they agree unit by unit; funext i turns a goal about functions into a goal about their values at an arbitrary i:

y1 y0 : Fin 3 → ℝ
h : ∀ (i : Fin 3), y1 i = y0 i
i : Fin 3
⊢ y1 i = y0 i

and then exact h i closes it, because h applied at that same i is literally the goal. Two lines: reduce the statement about functions to a statement about one value, then quote the hypothesis at that value.

ext is the general version, applying whatever extensionality lemma fits. For Finset — assignments, blocks, clusters — that is membership, so ext i reduces set equality to an equivalence of memberships.

1. ext i

   s = t between finsets becomes i ∈ s ↔ i ∈ t for a fresh i. The Finset extensionality lemma is what ext looked up; had the goal been an equality of functions it would have found funext instead, which is why ext is the one to reach for by default.

   Goal

   s t : Finset (Fin 3)
   h : ∀ (i : Fin 3), i ∈ s ↔ i ∈ t
   i : Fin 3
   ⊢ i ∈ s ↔ i ∈ t

2. exact h i

   h is exactly a family of such equivalences, one per unit, so h i is the goal. Two assignments are the same assignment when the same units are treated under both — and that sentence is the proof.

Chapter 12 needs this constantly, because a randomization test is a statement about sets of assignments.

Reading an error message

theorem mul_add_the_right_way (a b : ℝ) : a * (b + 1) = a * b + a := by
  rw [mul_add, mul_one]

The theorem itself is two rewrites, and both are needed.

1. rw [mul_add]

   mul_add : a * (b + c) = a * b + a * c distributes the product over the sum, so the goal’s left side becomes a * b + a * 1.

   Goal

   a b : ℝ
   ⊢ a * b + a * 1 = a * b + a

2. rw [mul_one]

   mul_one : a * 1 = a clears the unit factor, both sides become a * b + a, and rw closes the goal by reflexivity. A rw [x, y] list is exactly this: one rewrite after another, in the order written, each firing on what the previous one left.

Lean’s errors are long and formulaic, which means they are learnable. Two patterns cover most of the first week.

rewrite failed tells you the pattern it looked for and the expression it looked in:

error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  (?a + ?b) * ?c
in the target expression
  a * (b + 1) = a * b + a

The ?a, ?b are the lemma’s own variables waiting to be matched. Compare the pattern with your goal and the mismatch is usually visible in a second: here the lemma is add_mul, about (a + b) * c, and the goal has the factors the other way round, so mul_add is what was wanted. When the pattern does look like your goal but the rewrite still fails, the difference is typically implicit: a different type, a coercion, or an instance.

Open that block in the playground and change mul_add to add_mul if you want to watch it happen.

unsolved goals prints the state you were left in. That is a report, not a complaint: it is telling you exactly what remains.

error: unsolved goals
n k : ℕ
⊢ ↑(n - k) = ↑n - ↑k

Here push_cast did nothing, and the reason is mathematical — it refuses to push a cast through ℕ-subtraction, because the goal is false without k ≤ n. An error that says a tactic made no progress is frequently an error about your statement.

Finding the lemma

Mathlib has well over a hundred thousand theorems. You are not going to remember their names, and you do not have to: four tactics search for you.

theorem sum_of_squares_nonneg (x : ℝ) : 0 ≤ x ^ 2 := by
  exact sq_nonneg x

theorem sum_add (s : Finset (Fin 5)) (f g : Fin 5 → ℝ) :
    ∑ i ∈ s, (f i + g i) = ∑ i ∈ s, f i + ∑ i ∈ s, g i := by
  exact Finset.sum_add_distrib

theorem sum_div_two (a b c : ℝ) : (a + b) / c = a / c + b / c := by
  rw [add_div]

theorem sub_nonpos_of_le (x y : ℝ) (h : x ≤ y) : x - y ≤ 0 := by
  exact sub_nonpos.mpr h

• exact? looks for a single lemma that closes the goal outright.
• apply? looks for lemmas whose conclusion matches, leaving subgoals.
• simp? runs simp and prints the simp only [...] it actually used.
• rw? lists the rewrites that apply to the current goal.

The four theorems in that block are the four answers such a search returns, and each is one line.

1. exact sq_nonneg x

   sq_nonneg x : 0 ≤ x ^ 2 is the goal outright. This is the shape exact? reports most often: the fact was already in the library under a guessable name.

2. exact Finset.sum_add_distrib

   Chapter 3’s splitting lemma, applied with every argument implicit — the index set and the two functions are all determined by the goal, so the name alone is the proof.

3. rw [add_div]

   add_div : (a + b) / c = a / c + b / c. Here the answer is a rewrite rather than a term: after it fires, both sides of the goal are identical and rw closes it. rw? is the tactic that would have suggested it.

4. exact sub_nonpos.mpr h

   sub_nonpos : a - b ≤ 0 ↔ a ≤ b, so the goal is its left side and h is its right, which means .mpr. Note the caveat below: simp? on this goal offers a different route, and picking the ↔ lemma and the projection you want is the part a search tactic cannot do for you.

The workflow is: get the goal into the shape you believe is a known fact, run exact?, read what comes back, and paste the answer in. Leaving a search tactic in finished code is slow and fragile; they are development tools, like a debugger, not part of the program.

Two caveats, both visible in the block above. The search tactics find a proof, not the proof: simp? on x - y ≤ 0 reports a rewrite that leaves you with x ≤ y, when the lemma you actually wanted was sub_nonpos. And they only search for what you asked: if the goal is subtly the wrong statement, exact? failing tells you nothing about whether the right statement is provable.

Which tactic when

Exercises

theorem ex_intro_exact (y1 y0 : Fin 3 → ℝ) : (∀ i, y0 i ≤ y1 i) → y0 2 ≤ y1 2 := by
  sorry

theorem ex_intro_exact (y1 y0 : Fin 3 → ℝ) : (∀ i, y0 i ≤ y1 i) → y0 2 ≤ y1 2 := by
  intro h
  exact h 2

theorem ex_mean_le (a b : ℝ) (h : a ≤ b) : (a + b) / 2 ≤ b := by
  sorry

theorem ex_mean_le (a b : ℝ) (h : a ≤ b) : (a + b) / 2 ≤ b := by
  linarith

theorem ex_deviation_sq (x m : ℝ) :
    (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2 := by
  sorry

theorem ex_deviation_sq (x m : ℝ) :
    (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2 := by
  ring

theorem ex_sharp_null (y1 y0 : Fin 3 → ℝ) (h : ∀ i, y1 i = y0 i) :
    y1 0 - y0 0 = 0 := by
  sorry

theorem ex_sharp_null (y1 y0 : Fin 3 → ℝ) (h : ∀ i, y1 i = y0 i) :
    y1 0 - y0 0 = 0 := by
  rw [h 0, sub_self]

theorem ex_exists_pos (y1 y0 : Fin 3 → ℝ) (h : ∃ i, y1 i - y0 i = 2) :
    ∃ i, 0 < y1 i - y0 i := by
  sorry

theorem ex_exists_pos (y1 y0 : Fin 3 → ℝ) (h : ∃ i, y1 i - y0 i = 2) :
    ∃ i, 0 < y1 i - y0 i := by
  obtain ⟨i, hi⟩ := h
  use i
  rw [hi]
  norm_num

theorem ex_mean_clear (s n m : ℝ) (hn : n ≠ 0) (h : s / n = m) : s = n * m := by
  sorry

theorem ex_mean_clear (s n m : ℝ) (hn : n ≠ 0) (h : s / n = m) : s = n * m := by
  field_simp at h
  exact h

theorem ex_indicator_idempotent (i : Fin 4) (z : Finset (Fin 4)) :
    (if i ∈ z then (1 : ℝ) else 0) ^ 2 = if i ∈ z then (1 : ℝ) else 0 := by
  sorry

theorem ex_indicator_idempotent (i : Fin 4) (z : Finset (Fin 4)) :
    (if i ∈ z then (1 : ℝ) else 0) ^ 2 = if i ∈ z then (1 : ℝ) else 0 := by
  by_cases h : i ∈ z
  · rw [ite_eq_left h, one_pow]
  · rw [ite_eq_right h]; norm_num

Reading autoformalized Lean

Tactics make it easy to close a goal without noticing what the goal said. Both of the following compile, and both are worthless in a way the compiler cannot see.

The habit both pitfalls point to is the same one: when you are handed a formalization, read the statement, decide what it should require, and only then look at the proof. A tactic script is a plausible-looking artefact even when it is proving nothing at all.

Next: ℝ, Finset, and the sums that every result in Part II is made of.