Lean documentation

A Lean proof is a conversation between two lists: the assumptions we may use and the goal we must prove. The outermost logical operator tells us what to try next.

This guide explains the techniques in our numbered class and exercise files through Day 20. For commands at a glance, use the Lean reference.

This is the same viewpoint developed in Section 1.1 of Clive Newstead's An Infinite Descent into Pure Mathematics. An introduction rule explains how to prove a proposition containing an operator; an elimination rule explains how to use an assumption containing that operator. Lean makes those two moves visible.

Setup for the web editor

The Lean web editor cannot import our local macros.lean file. Copy the entire block below to the top of the editor instead. It defines the readable tactics used in these examples and declares P, Q, R, and S to be propositions.

macro "conj_elim" hp:ident hq:ident "from" h:ident : tactic =>
  `(tactic|(have ⟨$hp,$hq⟩ := $h))

macro "conj_intro" h:ident "from" hp:ident hq:ident : tactic =>
  `(tactic|(have $h : _∧_ := And.intro $hp $hq))

macro "disj_elim" hp:ident hq:ident "from" h:term:arg : tactic =>
  `(tactic|(refine Or.elim $h (fun $hp => ?_) (fun $hq => ?_)))

macro "disj_intro_left" h:ident "from" hp:ident q:term:arg : tactic =>
  `(tactic|(have $h : _∨($q) := Or.inl $hp))

macro "disj_intro_right" h:ident "from" p:term:arg hq:ident : tactic =>
  `(tactic|(have $h : ($p)∨_ := Or.inr $hq))

macro "impl_elim" hq:ident "from" hp:ident hpq:ident : tactic =>
  `(tactic|(have $hq := $hpq $hp))

variable (P Q R S : Prop)

Typing logical symbols

Lean source uses symbols such as ∧ and →, but you do not need to find them in a character picker. In the Lean editor, type a backslash command and then press Space (or Tab) to complete it.

For example, typing P \and Q \to R and completing each command produces P ∧ Q → R. Use parentheses whenever they make the intended logical structure clearer. The worked proofs below use conjunction, implication, disjunction, and negation.

First, read the proof state

After Lean enters proof mode at by, it displays assumptions above a turnstile and the current goal below it. For

example (h : P ∧ Q) : Q ∧ P := by

we may read the state schematically as

h : P ∧ Q
⊢ Q ∧ P

The assumption begins with a conjunction, so it can be eliminated. The goal begins with a conjunction, so it can be introduced. That observation is already a proof plan.

Keep an unfinished goal visible

In the web editor, pressing Enter after a tactic moves the cursor onto a position that does not yet contain a tactic. The Tactic state panel may become empty even though the goal is still present; the unfinished goal then appears in All Messages. To keep the current goal visible while building a proof, leave a sorry placeholder after the tactics you have written and put the cursor on sorry.

case inl hp =>
  apply Or.intro_right
  sorry  -- Keep this placeholder until the branch is complete.

Here apply Or.intro_right changes the goal from Q ∨ P to P. Putting the cursor on sorry displays that goal. Replace sorry with exact hp when you are ready to finish the branch.

Conjunction: “and”

Use a conjunction: conj_elim

The command conj_elim hp hq from h takes apart h : P ∧ Q. It adds two new facts, hp : P and hq : Q, to our assumptions.

Build a conjunction: conj_intro

If we already have proofs of both parts, conj_intro hqp from hq hp combines them and names the resulting proof hqp. Finally, exact hqp closes the goal because hqp has exactly the required type.

example (h : P ∧ Q) : Q ∧ P := by
  conj_elim hp hq from h
  conj_intro hqp from hq hp
  exact hqp

This proof increases our stock of known facts until one of them matches the goal. The two custom commands are readable names for conjunction elimination and introduction; they are defined in macros.lean using Lean's underlying rules.

Let the goal lead: apply And.intro

We can instead work backward from the goal. Applying the conjunction introduction rule to the goal Q ∧ P replaces it with two smaller goals, first Q and then P.

example (h : P ∧ Q) : Q ∧ P := by
  conj_elim hp hq from h
  apply And.intro
  exact hq
  exact hp

In textbook language, apply And.intro implements Strategy 1.1.7, proving conjunctions, while conj_elim implements Strategy 1.1.9, assuming conjunctions.

Parentheses are logical structure

Conjunctions nest. The expression P ∧ Q ∧ R is read as P ∧ (Q ∧ R), so we eliminate it twice. The goal (P ∧ Q) ∧ R also contains two conjunctions, so we introduce twice.

example (h : P ∧ Q ∧ R) : (P ∧ Q) ∧ R := by
  conj_elim hp hqr from h
  conj_elim hq hr from hqr
  apply And.intro
  apply And.intro
  exact hp
  exact hq
  exact hr

Implication: “if … then …”

Prove an implication: intro

If the goal is P → R, intro hp follows the implication introduction rule: it temporarily assumes P, names that assumption hp, and leaves R as the new goal.

Use an implication: impl_elim

If hpq : P → Q and hp : P, then impl_elim hq from hp hpq deduces and names hq : Q. This is implication elimination, also called modus ponens in Section 1.1.

example (hpq : P → Q) (hqr : Q → R) : P → R := by
  intro hp
  impl_elim hq from hp hpq
  impl_elim hr from hq hqr
  exact hr

Here, intro corresponds to Strategy 1.1.22, proving implications, and each impl_elim corresponds to Strategy 1.1.25, assuming implications.

Use implications backward: apply

The same argument can be driven entirely by the goal. If the goal is R and we have hqr : Q → R, then apply hqr changes the goal to Q: proving Q will be enough. Another apply reduces that goal to P.

example (hpq : P → Q) (hqr : Q → R) : P → R := by
  intro hp
  apply hqr
  apply hpq
  exact hp

The forward version with impl_elim asks, “What can I deduce from my assumptions?” The backward version with apply asks, “What would be enough to prove my goal?” They use the same logical rule in opposite working directions.

Disjunction: “or”

Introduce a disjunction: choose a side

A conjunction requires proofs of both parts, but a disjunction requires a proof of only one part. If we have hp : P, then disj_intro_left hpq from hp Q builds and names a proof hpq : P ∨ Q. The final Q tells Lean what the other proposition is.

example (hp : P) : P ∨ Q := by
  disj_intro_left hpq from hp Q
  exact hpq

If instead we have hq : Q, we introduce the right side. Here the extra P tells Lean what proposition belongs on the left.

example (hq : Q) : P ∨ Q := by
  disj_intro_right hpq from P hq
  exact hpq

These are the two disjunction introduction rules. In the textbook, they lead to Strategy 1.1.13: to prove P ∨ Q, it suffices to prove one of P or Q. Which side you choose matters—you should choose a side that your assumptions allow you to prove.

Eliminate a disjunction: proof by cases

Something new happens when eliminating a disjunction. If we know P ∨ Q, then we only know that at least one of P or Q is true, but we don't know which one. The only way we can prove a statement R in this situation is if we can prove it both from P and from Q. This means that the elimination rule for disjunctions produces two goals:

1. In the first case, Lean gives us hp : P.
2. In the second case, Lean gives us hq : Q.

We must prove the original goal in both cases. For example, disjunction is commutative:

example (h : P ∨ Q) : Q ∨ P := by
  disj_elim hp hq from h
  disj_intro_right hqp from Q hp
  exact hqp
  disj_intro_left hqp from hq P
  exact hqp

In the P case, we prove Q ∨ P using its right side. In the Q case, we prove the same goal using its left side. This is disjunction elimination, the proof-by-cases method described in Strategy 1.1.16. A case split succeeds only when every case reaches the same goal.

Use Lean's cases tactic

The tactic cases h also eliminates h : P ∨ Q. Lean names the two possible ways a proof of a disjunction can have been constructed: inl for a proof coming from the left and inr for a proof coming from the right. The corresponding case blocks focus on one goal at a time and give names to the new assumptions.

example (h : P ∨ Q) : Q ∨ P := by
  cases h
  case inl hp =>
    apply Or.intro_right
    exact hp
  case inr hq =>
    apply Or.intro_left
    exact hq

In case inl hp, Lean gives us hp : P; in case inr hq, it gives us hq : Q. Both branches must prove the original goal Q ∨ P. The names Or.intro_right and Or.intro_left are longer forms of Or.inr and Or.inl.

While constructing either branch in the web editor, keep sorry as its final line until the branch is finished. This prevents an incomplete branch from being reported only under All Messages and gives you a place where the current goal remains visible.

Let the goal lead with apply

As with conjunction and implication, we can work backward from a disjunction goal. If the goal is Q ∨ P, then apply Or.inr chooses the right alternative and changes the goal to P. Similarly, apply Or.inl chooses the left alternative and changes the goal to Q.

example (h : P ∨ Q) : Q ∨ P := by
  disj_elim hp hq from h
  apply Or.inr
  exact hp
  apply Or.inl
  exact hq

The two proofs of commutativity make the same logical moves. The first builds and names each new disjunction before using exact; the second simplifies each goal directly with apply.

Disjunctions can be nested

Lean reads P ∨ Q ∨ R as P ∨ (Q ∨ R). In the next example, eliminating hpq : P ∨ Q produces two cases. If P is true, introduce the left side of the goal. If Q is true, the assumption hqr : Q ∨ R already proves the entire right side, so introduce that side.

example (hpq : P ∨ Q) (hqr : Q ∨ R) : P ∨ Q ∨ R := by
  disj_elim hp hq from hpq
  disj_intro_left h from hp (Q ∨ R)
  exact h
  disj_intro_right h from P hqr
  exact h

The parenthesized argument (Q ∨ R) tells disj_intro_left the complete proposition on the right. This is another reason to keep track of how the operators are grouped.

A case that leads to contradiction

Lean treats ¬ P as P → False. Suppose we know ¬ P ∨ Q and want to prove P → Q. After assuming P, eliminate the disjunction:

• In the ¬ P case, implication elimination combines P and ¬ P to produce False. The tactic exfalso changes the current goal from Q to False, which we can prove with that contradiction.
• In the Q case, the assumption hq : Q is already exactly the goal.

example (h : ¬ P ∨ Q) : P → Q := by
  intro hp
  disj_elim hnp hq from h
  impl_elim f from hp hnp
  exfalso
  exact f
  exact hq

This proof combines implication introduction, disjunction elimination, implication elimination, and the principle that a contradiction implies any proposition. It also illustrates why both branches of a case split must be completed even when they finish in different ways.

Negation and contradiction

Reveal the implication with change

In Lean, ¬ P is notation for P → False. The change tactic replaces a goal or assumption by an equal expression that makes its useful logical structure visible. It does not change what must be proved.

example : ¬ (P ∧ ¬ P) := by
  change P ∧ ¬ P → False
  intro h
  conj_elim hp hnp from h
  change P → False at hnp
  apply hnp
  exact hp

The first change exposes the implication hidden in the goal. After intro h and conjunction elimination, the second change exposes the implication hidden in hnp : ¬ P. Applying hnp changes the goal from False to P, which is exactly the assumption hp.

The same idea proves the contrapositive form used in Lecture 5:

example (h : P → Q) (hnq : ¬ Q) : ¬ P := by
  change P → False
  intro hp
  change Q → False at hnq
  apply hnq
  apply h
  exact hp

Eliminate False

A proof of False has no possible cases. Therefore, if h : False, the command cases h closes any goal without producing a new branch. This is the principle that a contradiction implies anything.

example : False → P := by
  intro h
  cases h

If the current goal is some proposition Q and you intend to derive a contradiction, exfalso changes the goal to False. This is the goal-oriented form of the same principle.

Classical reasoning and excluded middle

Lean's core logic does not assume that every proposition is either true or false. After open Classical, the theorem em P supplies a proof of the law of excluded middle, P ∨ ¬ P.

open Classical

example : P ∨ ¬ P := by
  exact em P

Because em P is a disjunction, we can use cases em P to divide a classical proof into the case where P holds and the case where ¬ P holds.

example (h : P → Q) : ¬ P ∨ Q := by
  cases em P
  case inl hp =>
    apply Or.intro_right
    apply h
    exact hp
  case inr hnp =>
    apply Or.intro_left
    exact hnp

Mixing the operators

Real proofs alternate between introduction and elimination. To prove P → Q → R, introduce its two implications. Then build the conjunction required by the assumed implication P ∧ Q → R, use that implication, and finish with the result.

example (h : P ∧ Q → R) : P → Q → R := by
  intro hp
  intro hq
  conj_intro hpq from hp hq
  impl_elim hr from hpq h
  exact hr

If and only if: prove both directions

The goal P ↔ Q requires two implications. apply Iff.intro creates them. A line beginning with show can state the current goal explicitly, as in Day 6; it does not prove that goal.

example (hpq : P → Q) (hqp : Q → P) : P ↔ Q := by
  apply Iff.intro
  · show P → Q
    exact hpq
  · show Q → P
    exact hqp

To use h : P ↔ Q, h.mp is the implication P → Q, and h.mpr is Q → P. Thus exact h.mpr hq proves P from hq : Q. Day 8 uses P_iff_neg_neg_P.mpr to turn a proof of ¬ ¬ P into a proof of P.

Prove a positive statement by contradiction

To prove ¬ P, we already know to assume P and derive False. Classical proof by contradiction lets us prove P by assuming ¬ P and deriving False. After open Classical, write apply byContradiction followed by intro hnp.

open Classical

example (hnnp : ¬ ¬ P) : P := by
  apply byContradiction
  intro hnp
  contradiction

Here the new assumption hnp : ¬ P contradicts hnnp : ¬ ¬ P. The same method appears inside the quantified proofs below.

Quantifiers: arbitrary elements and witnesses

Write T : Type for the type of objects we are discussing, t : T for an object of that type, and P : T → Prop for a property of those objects. Then P t is a proposition. In these examples, P and Q are properties, rather than the fixed propositions used above.

Prove a universal statement with intro

To prove ∀ x : T, P x, introduce an arbitrary t : T and prove P t. You cannot choose a convenient value of t: your argument must work for the arbitrary element Lean gives you. In a goal ∀ x : T, P x → Q x, first introduce the element, then the hypothesis:

example {T : Type} {P Q : T → Prop}
    (h : ∀ x : T, P x → Q x) : ∀ x : T, P x → Q x := by
  intro t
  intro hpt
  have hptqt := h t
  apply hptqt
  exact hpt

After intro t, the goal is P t → Q t. After intro hpt, it is Q t. intro t hpt combines those two lines.

Use a universal statement by giving it an argument

If h : ∀ x : T, P x and t : T, then h t proves P t. You can record it with have hpt := h t, or finish directly with exact h t. If h : ∀ x : T, P x → Q x, then h t is an implication; supplying a second argument, h t hpt, proves Q t.

example {T : Type} {P Q R : T → Prop}
    (h₁ : ∀ x : T, P x → Q x)
    (h₂ : ∀ x : T, P x → R x) :
    ∀ x : T, P x → Q x ∧ R x := by
  intro t hpt
  apply And.intro
  · exact h₁ t hpt
  · exact h₂ t hpt

Each quantified hypothesis is specialized to the same t that we introduced for the goal. The dots keep the two conjunction goals separate.

Prove an existential statement by choosing a witness

To prove ∃ x : T, P x, supply a particular t : T with apply Exists.intro t. The goal becomes P t. Unlike a universal proof, an existential proof lets you choose the value.

example {T : Type} {P : T → Prop} (t : T) (hpt : P t) :
    ∃ x : T, P x := by
  apply Exists.intro t
  exact hpt

If both the witness and its proof are already available, exact ⟨t, hpt⟩ is the short version from Day 8.

Use an existential statement by opening its witness

From h₁ : ∃ x : T, P x, obtain ⟨t, hpt⟩ := h₁ gives a witness t : T and hpt : P t. The form have ⟨t, hpt⟩ := h₁ also appears in Day 10. The witness is supplied by the assumption; you cannot require it to be a particular value of your choosing.

example {T : Type} {P Q : T → Prop}
    (h₁ : ∃ x : T, P x) (h₂ : ∀ x : T, Q x) :
    ∃ x : T, P x ∧ Q x := by
  obtain ⟨t, hpt⟩ := h₁
  apply Exists.intro t
  apply And.intro
  · exact hpt
  · exact h₂ t

We reuse that witness to prove the new existential goal. The universal assumption supplies Q t for this very same t. To write the witness-opening step in the longer form used in class:

example {T : Type} {P : T → Prop} {Q : Prop}
    (h₁ : ∃ x : T, P x) (h₂ : ∀ x : T, P x → Q) : Q := by
  apply Exists.elim h₁
  intro t
  intro hpt
  exact h₂ t hpt

The conclusion is still Q. The introduced witness and its property are available while proving that conclusion.

Recursively defined functions

Load the natural numbers used in class

The remaining examples use our custom ℕ from natural_numbers.lean. In the local course project, put import natural_numbers at the top of your file. In the web editor, paste the contents of that file first, then add the examples below. It supplies ℕ, addition, multiplication, and the arithmetic theorems used here. Type \N and complete it to insert ℕ.

Our numbers are built from ℕ.zero and ℕ.succ. The notation n.succ means ℕ.succ n. Thus ℕ.zero.succ.succ is two. We can also write numerals, with a type annotation such as (2 : ℕ) when needed. Earlier files used Nat; these examples follow the custom ℕ used in the later classes.

Give a starting value and a rule for the next value

The function from Days 18–20 starts at zero and adds two successors each time its input increases by one:

def f : ℕ → ℕ
  | ℕ.zero => ℕ.zero
  | ℕ.succ n => (f n).succ.succ

The first line says that f takes a natural number and returns a natural number. The first case specifies f ℕ.zero. The second says how to compute f n.succ once we know f n. The recursive call uses the preceding input n.

Day 17 writes the same kind of definition with match. Here is that format applied to the same rule, under a different name:

def f_match (n : ℕ) : ℕ := match n with
  | .zero => ℕ.zero
  | .succ k => (f_match k).succ.succ

For this match, .zero and .succ are the short forms of ℕ.zero and ℕ.succ. Both presentations give a zero rule and a successor rule.

Compute examples with #eval

#eval f 2

example : f (2 : ℕ) = (4 : ℕ) := by
  rfl

#eval computes the value and shows it in the messages. Our custom natural numbers may be displayed as nested zero/successor constructors. The example below it proves the particular equality by computation: rfl succeeds because both sides reduce to the same value. Checking a few inputs is useful, but a claim about every input needs a proof for arbitrary n.

Name the defining equations

theorem f_zero : f ℕ.zero = ℕ.zero := by
  rfl

theorem f_succ (n : ℕ) : f n.succ = (f n).succ.succ := by
  rfl

These statements are exactly the two rules in the definition. rfl proves each one. The names let us use the equations in later proofs with rewrite [f_zero] and rewrite [f_succ]. We can also expose the rule directly with unfold f or rewrite [f], as in Day 20.

Addition and multiplication recurse on their first input

The support file defines plus and times by these equations. They are already loaded; you can read the definitions without entering them again:

def plus : ℕ → ℕ → ℕ
  | ℕ.zero, n => n
  | ℕ.succ m, n => ℕ.succ (plus m n)

def times : ℕ → ℕ → ℕ
  | ℕ.zero, _ => ℕ.zero
  | ℕ.succ m, n => plus n (times m n)

The wildcard _ marks an input whose value is not needed in that case: zero times any number is zero. Write plus m n as m + n and times m n as m * n. Parentheses make the grouping explicit.

Because these definitions examine the first input, ℕ.zero + n = n follows directly by computing the zero rule. But n + ℕ.zero = n requires an argument about the unknown first input n. This is where induction helps.

Induction with induction n using ℕ.rec

If the goal starts with ∀ n : ℕ, ..., first use intro n. If n is already a theorem parameter, it is already available. Then write induction n using ℕ.rec. Lean creates two goals:

The name ih is our name for the induction hypothesis. It is available only in the successor branch. Read its type in the proof state: that tells you exactly what you may use.

Example: adding zero on the right

example : ∀ n : ℕ, n + ℕ.zero = n := by
  intro n
  induction n using ℕ.rec
  case zero =>
    unfold plus
    rfl
  case succ n ih =>
    unfold plus
    rewrite [ih]
    rfl

In the zero branch, unfold plus exposes the starting rule, leaving the same number on both sides. In the successor branch, the important part of the state is:

n : ℕ
ih : n + ℕ.zero = n
⊢ n.succ + ℕ.zero = n.succ

Unfolding the definition changes the goal to (n + ℕ.zero).succ = n.succ. Now rewrite [ih] replaces n + ℕ.zero with n, and rfl finishes n.succ = n.succ. The induction hypothesis applies to the smaller input after the recursive rule has exposed it.

Example: commutativity needs earlier lemmas

Choose the induction variable to match the first input of plus. In the successor branch, the two sides need different equations: succ_plus handles a successor on the left of addition, and plus_succ handles one on the right.

example (m n : ℕ) : m + n = n + m := by
  induction m using ℕ.rec
  case zero =>
    rewrite [zero_plus, plus_zero]
    rfl
  case succ m ih =>
    rewrite [succ_plus, plus_succ]
    rewrite [ih]
    rfl

After the successor rewrites, the goal is (m + n).succ = (n + m).succ. The induction hypothesis is exactly m + n = n + m. Earlier lemmas let us arrange the goal so that the hypothesis can be used.

Example: the recursively defined function doubles its input

For the f defined above, we can prove the formula from Days 19–20. The imported file supplies the multiplication and addition lemmas:

theorem f_doubles (n : ℕ) : f n = n * (2 : ℕ) := by
  induction n using ℕ.rec
  case zero =>
    rewrite [f_zero, zero_times]
    rfl
  case succ n ih =>
    rewrite [f_succ, succ_times]
    change (f n).succ.succ = ℕ.zero.succ.succ + n * (2 : ℕ)
    rewrite [succ_plus, succ_plus, zero_plus]
    rewrite [ih]
    rfl

In the successor branch, expose the successor equations for both f and multiplication. Express two as two successors of zero and use the addition rules. Both sides now have two outer successors, so rewriting f n using ih finishes the argument.

Negating quantifiers

The class proofs establish (¬ ∃ x : T, P x) ↔ (∀ x : T, ¬ P x) and, using classical reasoning, (¬ ∀ x : T, P x) ↔ (∃ x : T, ¬ P x). Read these as “there is no example” and “there is a counterexample,” respectively. To prove that there is no example, open an alleged witness and contradict the corresponding universal fact:

example {T : Type} {P : T → Prop}
    (h : ∀ x : T, ¬ P x) : ¬ ∃ x : T, P x := by
  intro h₁
  obtain ⟨t, hpt⟩ := h₁
  have hnpt := h t
  contradiction

In the other direction, build the existential statement that would contradict the assumption. This illustrates an intermediate proof with have ... := by:

example {T : Type} {P : T → Prop}
    (h : ¬ ∃ x : T, P x) : ∀ x : T, ¬ P x := by
  intro t
  intro hpt
  have h₁ : ∃ x : T, P x := by
    apply Exists.intro t
    exact hpt
  contradiction

A counterexample refutes a universal statement: given ∃ x : T, ¬ P x, open its witness, assume ∀ x : T, P x, specialize that assumption to the witness, and use contradiction. To obtain a counterexample from a failed universal statement, Days 8 and 12 use proof by contradiction twice:

open Classical

example {T : Type} {P : T → Prop}
    (h : ¬ ∀ x : T, P x) : ∃ x : T, ¬ P x := by
  apply byContradiction
  intro h₁
  apply h
  intro t
  apply byContradiction
  intro hnpt
  apply h₁
  apply Exists.intro t
  exact hnpt

First assume there is no counterexample. To contradict h, prove ∀ x : T, P x. For an arbitrary t, assume ¬ P t; then t itself would be the counterexample ruled out by h₁.

Practical tools for equality proofs

rfl, unfold, and change

rfl closes an equality when the sides are identical after computing definitions. unfold f exposes a definition in the goal. change writes the same goal in another form justified by definitions, as with ¬ P and P → False earlier. It cannot substitute an arithmetic theorem that still needs to be proved.

example (n : ℕ) : (2 : ℕ) * n = n + n := by
  change ℕ.zero.succ.succ * n = n + n
  unfold times
  unfold times
  unfold times
  rewrite [plus_zero]
  rfl

This is the two_times argument from Day 20. Writing two as successors exposes three applications of the multiplication definition. The remaining expression is n + (n + ℕ.zero); plus_zero removes the final zero.

Rewrite in the direction and instance you need

If ih : f n = n * (2 : ℕ), rewrite [ih] replaces a matching f n in the goal by n * (2 : ℕ). A list such as rewrite [f_zero, zero_times] applies the rewrites in order. rewrite may leave an equality with identical sides; then use rfl.

Prefix a theorem with ← to use it in reverse. Our plus_assoc a b c says a + (b + c) = (a + b) + c. Supplying its arguments chooses the grouping you want to change:

example (a b c : ℕ) : (a + b) + c = a + (b + c) := by
  rewrite [← plus_assoc a b c]
  rfl

Type \l to insert ←. Explicit arguments are especially useful with plus_comm: they identify which two summands should be swapped in a larger expression.

Prove a small rewriting equation inline

Days 19 and Exercise 18 use show ... by rfl inside a rewrite list. It supplies a small equality immediately, without naming a separate theorem:

example (n : ℕ) : (2 : ℕ) * n = n + n := by
  rewrite [show (2 : ℕ) = ℕ.zero.succ.succ by rfl]
  unfold times
  unfold times
  unfold times
  rewrite [plus_zero]
  rfl

For a longer intermediate argument, use have : ... := by and refer to the resulting equality as this, or give it a name. Day 19 uses this to establish the same identity before continuing a larger proof.

Focus on part of an equality with conv

Sometimes unfolding both sides obscures the step you want. The class command conv => lhs ; unfold plus selects the left side of the equality and unfolds only there:

example (n : ℕ) : ℕ.zero + n = n := by
  conv => lhs ; unfold plus

Use rhs to select the right side. Then arg 1 selects its first argument. In Day 20, the right side is an addition whose first argument is n.succ; the command changes just that argument to (1 : ℕ) + n:

example (n t : ℕ) : ((1 : ℕ) + n) + t = n.succ + t := by
  conv => rhs ; arg 1 ; change (1 : ℕ) + n

The semicolons here separate the successive focusing commands. Once that selected expression has been changed, Lean returns to the surrounding equality.

Reduce equality of function values with congrArg

In Exercise 18, both sides sometimes have the same outer successor or the same added term. apply congrArg reduces the goal to equality of their inputs:

example (a b : ℕ) (h : a = b) : a.succ = b.succ := by
  apply congrArg
  exact h

The same move can reduce n + a = n + b to a = b. In the multiplication proofs, this exposes the part that needs associativity and commutativity rewrites.

Lean tactics and techniques

example (hp : P) (hpq : P → Q) : Q := by
  have := hpq hp
  exact this

example (h : P ∧ Q) : Q ∧ P := by
  have ⟨hp, hq⟩ := h
  exact ⟨hq, hp⟩

example (h : (P → R) ∧ (Q → R)) : P ∨ Q → R := by
  have ⟨hpr, hqr⟩ := h
  intro hpq
  rcases hpq with hp | hq
  · exact hpr hp
  · exact hqr hq

example (hp : P) (hq : Q) :
    ¬ (P ∧ Q) → (¬ P ∨ ¬ Q) := by
  simp [hp, hq]

example (a b c : ℕ) : a + (b + c) = (a + b) + c := by
  simp only [plus_assoc]

example (a b : ℕ) : a + b = b + a := by
  simp only [plus_comm]