Tactics

Chapter 1 built proofs by hand, as terms. That works up to about four lines and then stops being possible: nobody writes the proof term for a variance identity. What you write instead is a tactic script — a sequence of instructions that constructs the term for you — and by is the keyword that switches from one mode to the other.

The thing to understand about tactic mode is that the script is not the proof. The script is a program whose output is the proof, and the object you actually reason about while writing it is neither: it is the goal state. A goal state is a list of hypotheses and one conclusion, and every tactic is a transformation of it. Learning tactics is learning what each one does to the state, and the fastest way to learn that is to put the cursor on a line in the playground and look.

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

Above the turnstile, what you have. Below it, what you owe. A tactic either changes what you have, changes what you owe, or closes the goal. When there are no goals left the proof is finished.

Everything below is quoted from lean/MrCLean/Fundamentals/Ch02Tactics.lean, which CI compiles. Open the blocks in the playground and move the cursor down them line by line; reading this chapter without doing that is like reading about a debugger.

intro and exact

/-- A tactic proof is a sequence of instructions that transform a *goal state*.
The state is a list of hypotheses and one conclusion, displayed as

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

`intro` moves the antecedent of an `→` or a `∀` from the goal into the
hypotheses; `exact` supplies a term that closes the goal outright.  Put the
cursor at the end of any line in the playground to see the state there. -/
theorem effect_nonneg_at_zero (y1 y0 : Fin 3 → ℝ) :
    (∀ i, y0 i ≤ y1 i) → y0 0 ≤ y1 0 := by
  intro h        -- ⊢ y0 0 ≤ y1 0, with `h : ∀ i, y0 i ≤ y1 i` in context
  exact h 0      -- no goals

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 => …. Before:

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

After intro h:

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

exact e closes the goal with the term e, which must have exactly the goal’s type. exact h 0 applies the ∀ at unit 0, giving y0 0 ≤ y1 0, which is the goal. 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

/-- `apply f` works backwards: it replaces the goal by whatever `f` still needs.
Here `le_trans : a ≤ b → b ≤ c → a ≤ c` turns one goal into two. -/
theorem obs_le_of_le (a b c : ℝ) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by
  apply le_trans
  · exact hab
  · exact hbc

/-- `refine` is `exact` with holes: write the shape of the answer and leave `?_`
where you want a new goal.  This is the tactic to reach for when you know the
structure of the argument but not yet the details. -/
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.

refine is exact with holes. You write the shape of the answer and put ?_ where you want a new goal, so refine ⟨ha, ?_⟩ on the goal 0 ≤ a ∧ 0 ≤ a + b supplies the first component and leaves

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

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

/-- `rw [h]` replaces occurrences of the left-hand side of `h` by its right-hand
side, everywhere in the goal.  `rw [← h]` goes the other way.  Rewriting is the
workhorse: most statistical identities are chains of substitutions. -/
theorem obs_of_treated (y1 yobs : ℝ) (h : yobs = y1) (hy : y1 = 3) : yobs = 3 := by
  rw [h]         -- ⊢ y1 = 3
  exact hy

/-- `rw [← h]` uses the equation right-to-left: here we turn the `3` in the goal
back into `y1`, which is what the hypothesis talks about. -/
theorem obs_of_treated' (y1 yobs : ℝ) (h : yobs = y1) (hy : y1 = 3) : yobs = 3 := by
  rw [← hy]      -- ⊢ yobs = y1
  exact h

/-- `rw … at h` rewrites inside a hypothesis instead of the goal.  A typical use:
a constant-effects assumption is stated for all units, and you specialise it and
then rewrite the observed data with it. -/
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        -- h1 : y1 1 - y0 1 = c
  rw [hc] at h1         -- h1 : y1 1 - y0 1 = 2
  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.

On obs_of_treated, with h : yobs = y1 and goal yobs = 3, after rw [h]:

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

Three things about rw that are worth knowing on day one.

It goes left to right, and ← reverses it. rw [← hy] uses hy : y1 = 3 right-to-left, turning the 3 in the goal back into y1. 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. In effect_at_unit this specializes the constant-effects assumption at unit 1 and then substitutes the value of the constant:

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

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

/-- `simp` rewrites with the whole `@[simp]` database until nothing changes.  It
is convenient and opaque: for teaching material prefer `simp only [these, ones]`,
which says exactly which facts were used and does not drift when Mathlib
changes. -/
theorem sum_two_outcomes (y : Fin 3 → ℝ) : y 0 + 0 + (y 1 * 1) = y 0 + y 1 := by
  simp only [add_zero, mul_one]

/-- `simp at h` normalises a hypothesis rather than the goal. -/
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.

Building and taking apart

/-- `constructor` applies the constructor of an inductive goal: for `∧` it splits
the goal into the two conjuncts. -/
theorem both_nonneg (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a ∧ 0 ≤ b := by
  constructor
  · exact ha
  · exact hb

/-- For an `∃` goal, `use w` supplies the witness and leaves you with the
property.  Here: some unit in a three-unit study is treated. -/
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

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.

/-- `obtain ⟨i, hi⟩ := h` takes an `∃` (or an `∧`) apart.  `rcases h with ⟨i, hi⟩`
is the same tactic with a different spelling; `cases h with | intro i hi => …` is
the low-level version. -/
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⟩

/-- On a disjunction, `rcases … with h | h` gives one goal per case: exactly the
"treated or control" case split that pervades design-based arguments. -/
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

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

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

/-- `have` proves an intermediate fact and adds it to the context — the Lean
equivalent of "note that …".  `show` restates the goal in a definitionally equal
form, which is how you tell Lean (and the reader) what you think you are
proving. -/
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.

/-- `calc` writes a chain of equalities or inequalities the way you would on
paper, with the justification for each step on the right.  It is the single most
readable tactic and the one to prefer in anything anyone else will read. -/
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 is the one tactic that produces something worth reading. It writes a chain of equalities or inequalities the way you would on paper, with the justification for each step to the right of :=, and each _ standing for the previous right-hand side. The example is the decomposition $Z{y}_1+(1-Z)y_0=y_0+Z(y_1-y_0)$ that every discussion of potential outcomes starts from.

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.

/-- `ring` proves any identity that holds in every commutative ring: it
normalises both sides and compares.  Every "expand the square" step in a variance
calculation is a `ring` call. -/
theorem square_of_deviation (x m : ℝ) :
    (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2 := by ring

/-- `ring` knows nothing about hypotheses or inequalities — only identities. -/
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.

/-- `linarith` closes any goal that follows from the hypotheses by *linear*
arithmetic over an ordered field: adding inequalities and scaling them by
positive constants. -/
theorem mean_between (a b : ℝ) (hab : a ≤ b) : a ≤ (a + b) / 2 := by linarith

/-- `nlinarith` is `linarith` plus some products of hypotheses; it is what to try
when the goal is genuinely nonlinear, e.g. a variance-style bound. -/
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.

/-- `positivity` proves goals of the form `0 < e`, `0 ≤ e` or `e ≠ 0` by walking
the syntax of `e`.  Sums of squares and sample sizes are its bread and butter. -/
theorem variance_denominator_pos (n : ℕ) (hn : 0 < n) : 0 < (n : ℝ) ^ 2 + 1 := by
  positivity

/-- `field_simp` clears denominators, given that they are nonzero.  It is the
first move in any argument about a mean or a ratio estimator. -/
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.

/-- `norm_num` evaluates concrete numerals, in any of `ℕ`, `ℤ`, `ℚ`, `ℝ`. -/
theorem concrete_mean : ((2 : ℝ) + 4 + 6) / 3 = 4 := by norm_num

/-- `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 this comes up constantly. -/
theorem control_count (n n₁ : ℕ) (h : n₁ ≤ n) : n₁ + (n - n₁) = n := by omega

/-- `decide` evaluates a decidable proposition.  It works only when everything is
concrete and small — and it proves the claim *for that instance only*. -/
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.

/-- Sample sizes are natural numbers; means are real.  `(n : ℝ)` is a coercion,
printed `↑n`.  `push_cast` pushes coercions towards the leaves of an expression,
`norm_cast` tries to remove them altogether. -/
theorem cast_add (n₁ n₀ : ℕ) : ((n₁ + n₀ : ℕ) : ℝ) = (n₁ : ℝ) + (n₀ : ℝ) := by
  push_cast
  ring

/-- Subtraction is where casts bite.  `Nat.cast_sub` needs the hypothesis `k ≤ n`,
because `ℕ`-subtraction truncates at zero while `ℝ`-subtraction does not: without
`h`, the statement below is false at `n = 0, k = 1`. -/
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: push_cast refuses to move a cast through a ℕ-subtraction, because ((n - k : ℕ) : ℝ) = (n : ℝ) - k is false without k ≤ n. When a cast tactic makes no progress, suspect the statement before the tactic.

Case splits and contradictions

/-- `by_cases h : p` splits the proof into the case where `p` holds and the case
where it does not.  For an indicator this is the whole story: `Z i` is `1` on the
treated and `0` on the controls, so every fact about it is two computations. -/
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]     -- the treated branch: `1 * 1 = 1`
  · rw [ite_eq_right h, mul_zero]   -- the control branch: `0 * 0 = 0`

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, by ite_eq_left h and ite_eq_right h, which use that hypothesis to collapse the if — in the positive branch the goal becomes 1 * 1 = 1, in the negative one 0 * 0 = 0.

/-- `exfalso` replaces any goal by `False`: use it when you intend to derive a
contradiction from the hypotheses.  `contradiction` finds an outright
inconsistency in the context and closes the goal. -/
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)

/-- This is worth internalising before reading any autoformalized statement: a
theorem with contradictory hypotheses is *provable and worthless*.  Above, the
"conclusion" `1 = 2` was never touched. -/
theorem from_absurd_hypotheses' (n : ℕ) (h1 : 0 < n) (h2 : n = 0) : (1 : ℝ) = 2 := by
  subst h2
  contradiction

/-- `by_contra h` assumes the negation of the goal.  Useful when the direct proof
is awkward but the contradiction is immediate. -/
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.

Read the second theorem in that block twice. It proves (1 : ℝ) = 2 from 0 < n and n = 0, and the “conclusion” is never 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

/-- Two outcome vectors are equal exactly when they agree unit by unit.  `funext`
turns a goal about functions into a goal about their values. -/
theorem outcomes_eq (y1 y0 : Fin 3 → ℝ) (h : ∀ i, y1 i = y0 i) : y1 = y0 := by
  funext i
  exact h i

/-- `ext` is the general version: it applies whatever extensionality lemma fits
the goal.  For assignments — finite sets of treated units — that is membership. -/
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

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 i ∈ s ↔ i ∈ t. Chapter 12 needs this constantly, because a randomization test is a statement about sets of assignments.

Reading an error message

/-- Lean's errors are long but formulaic.  Two you will meet on day one, quoted
verbatim from this file's own failures.

**Rewrite failed.**  Asking for `rw [add_mul]` on the goal
`a * (b + 1) = a * b + a` gives

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

Read it as: the lemma is about `(a + b) * c`, your goal has `a * (b + 1)`, so the
*sides* are swapped.  `mul_add` is the lemma you wanted.  The metavariables `?a`,
`?b` are the lemma's own variables, waiting to be matched.

**Unsolved goals.**  Trying to prove `((n - k : ℕ) : ℝ) = (n : ℝ) - k` by
`push_cast; ring` gives

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

`push_cast` did nothing, which is the message: it *refuses* to push the cast
through a `ℕ`-subtraction, because the statement is false without `k ≤ n`.  The
error is telling you the mathematics is wrong, not that you picked the wrong
tactic. -/
theorem mul_add_the_right_way (a b : ℝ) : a * (b + 1) = a * b + a := by
  rw [mul_add, mul_one]

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.

/-- Four tactics search for you.  Run them in the playground, read what they
report, then paste the answer in: leaving a search tactic in finished code is
slow and fragile.

* `exact?` looks for a single lemma that closes the goal;
* `apply?` looks for lemmas that make progress;
* `simp?` runs `simp` and prints the `simp only [...]` it actually used;
* `rw?` lists rewrites that apply to the goal.

The comments below are what these tactics printed on these goals. -/
theorem sum_of_squares_nonneg (x : ℝ) : 0 ≤ x ^ 2 := by
  -- `exact?` reports:  Try this: exact sq_nonneg x
  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?` reports:  Try this: exact Finset.sum_add_distrib
  exact Finset.sum_add_distrib

theorem sum_div_two (a b c : ℝ) : (a + b) / c = a / c + b / c := by
  -- `rw?` reports:  Try this: rw [add_div]  -- no goals
  rw [add_div]

theorem sub_nonpos_of_le (x y : ℝ) (h : x ≤ y) : x - y ≤ 0 := by
  -- `simp?` reports:  Try this: simp only [tsub_le_iff_right, zero_add]
  -- which leaves `x ≤ y` — a reminder that the search tactics find *a* proof,
  -- not the proof you want.  The lemma you actually wanted is named:
  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 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 snippet. 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

/-- Exercise (warm-up).  Two tactics: move the hypothesis into the context, then
apply it at unit `2`. -/
theorem ex_intro_exact (y1 y0 : Fin 3 → ℝ) : (∀ i, y0 i ≤ y1 i) → y0 2 ≤ y1 2 := by
  sorry

/-- Exercise (warm-up).  Two tactics: move the hypothesis into the context, then
apply it at unit `2`. -/
theorem ex_intro_exact (y1 y0 : Fin 3 → ℝ) : (∀ i, y0 i ≤ y1 i) → y0 2 ≤ y1 2 := by
  intro h
  exact h 2

/-- Exercise (warm-up).  The sample mean of two numbers lies between them.  One
tactic. -/
theorem ex_mean_le (a b : ℝ) (h : a ≤ b) : (a + b) / 2 ≤ b := by
  sorry

/-- Exercise (warm-up).  The sample mean of two numbers lies between them.  One
tactic. -/
theorem ex_mean_le (a b : ℝ) (h : a ≤ b) : (a + b) / 2 ≤ b := by
  linarith

/-- Exercise (core).  The identity behind the computational formula for the
variance, one unit at a time.  One tactic. -/
theorem ex_deviation_sq (x m : ℝ) :
    (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2 := by
  sorry

/-- Exercise (core).  The identity behind the computational formula for the
variance, one unit at a time.  One tactic. -/
theorem ex_deviation_sq (x m : ℝ) :
    (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2 := by
  ring

/-- Exercise (core).  Under the sharp null of no effect, every unit's observed
outcome equals its control outcome.  Rewrite with the hypothesis and finish.
`rw [h]` where `h` is a `∀` needs the instance: `rw [h 0]`, or just `rw [h]`. -/
theorem ex_sharp_null (y1 y0 : Fin 3 → ℝ) (h : ∀ i, y1 i = y0 i) :
    y1 0 - y0 0 = 0 := by
  sorry

/-- Exercise (core).  Under the sharp null of no effect, every unit's observed
outcome equals its control outcome.  Rewrite with the hypothesis and finish.
`rw [h]` where `h` is a `∀` needs the instance: `rw [h 0]`, or just `rw [h]`. -/
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]

/-- Exercise (core).  From "some unit has effect exactly `2`" conclude "some unit
has a positive effect".  `obtain ⟨i, hi⟩ := h` takes the witness apart; `exact
⟨i, _⟩` or `use i` puts one back. -/
theorem ex_exists_pos (y1 y0 : Fin 3 → ℝ) (h : ∃ i, y1 i - y0 i = 2) :
    ∃ i, 0 < y1 i - y0 i := by
  sorry

/-- Exercise (core).  From "some unit has effect exactly `2`" conclude "some unit
has a positive effect".  `obtain ⟨i, hi⟩ := h` takes the witness apart; `exact
⟨i, _⟩` or `use i` puts one back. -/
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

/-- Exercise (core).  Clear the denominator.  `field_simp` needs to know the
denominator is nonzero — the hypothesis `hn` is already in the context, and
`field_simp` will look for it.  Note the order of the product it leaves you
with: `field_simp` normalises, it does not read your mind. -/
theorem ex_mean_clear (s n m : ℝ) (hn : n ≠ 0) (h : s / n = m) : s = n * m := by
  sorry

/-- Exercise (core).  Clear the denominator.  `field_simp` needs to know the
denominator is nonzero — the hypothesis `hn` is already in the context, and
`field_simp` will look for it.  Note the order of the product it leaves you
with: `field_simp` normalises, it does not read your mind. -/
theorem ex_mean_clear (s n m : ℝ) (hn : n ≠ 0) (h : s / n = m) : s = n * m := by
  field_simp at h
  exact h

/-- Exercise (stretch).  The indicator is idempotent: `Z² = Z`, because `0² = 0`
and `1² = 1`.  Split on membership with `by_cases h : i ∈ z`, then evaluate the
`if` in each branch (`if_pos h` / `if_neg h`, or `simp [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

/-- Exercise (stretch).  The indicator is idempotent: `Z² = Z`, because `0² = 0`
and `1² = 1`.  Split on membership with `by_cases h : i ∈ z`, then evaluate the
`if` in each branch (`if_pos h` / `if_neg h`, or `simp [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
  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.