2.17 Proof Structuring Patterns

A Lean proof should expose the shape of the argument. The goal is not merely to make the theorem compile. The goal is to make the proof local, stable, and readable when the surrounding file changes.

Problem

You have a theorem that can be proved in several ways, but the proof becomes hard to read because assumptions, intermediate facts, and final construction steps are mixed together.

Solution

Use a simple proof structure:

Introduce assumptions
Destructure compound hypotheses
Prove intermediate facts with have
Build the final goal
Use automation only where the intended step is clear

For example:

theorem structured_example
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  have hq : Q := hPQ hp
  have hr : R := hQR hq
  exact hr

This proof names each logical step. It is longer than necessary, but it is easy to inspect.

Compact Version

The same theorem can be proved in one line:

theorem compact_example
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  exact hQR (hPQ hp)

This version is fine when the composition is obvious. Prefer the structured version when the intermediate terms carry mathematical meaning or when the proof is likely to grow.

Introduce First

For theorems with implication or universal quantification, introduce the variables and assumptions before doing serious work.

theorem introduce_first
    (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hPQ
  intro hQR
  intro hp
  exact hQR (hPQ hp)

A shorter form is also common:

theorem introduce_first_short
    (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hPQ hQR hp
  exact hQR (hPQ hp)

Use one name per logical object. Avoid names such as h, h1, and h2 when the proof is longer than a few lines.

Destructure Early

If a hypothesis contains a conjunction or existential, unpack it near the beginning of the proof.

theorem destructure_early
    (P Q R : Prop)
    (h : P ∧ Q)
    (hQR : Q -> R) :
    P ∧ R := by
  rcases h with ⟨hp, hq⟩
  have hr : R := hQR hq
  exact ⟨hp, hr⟩

This makes the available facts explicit:

hp : P
hq : Q
hr : R

The final construction then reads directly.

Keep Case Branches Symmetric

When using a disjunction, each branch should have a similar shape.

theorem branch_structure
    (P Q R : Prop)
    (h : P ∨ Q)
    (hPR : P -> R)
    (hQR : Q -> R) :
    R := by
  cases h with
  | inl hp =>
    exact hPR hp
  | inr hq =>
    exact hQR hq

The branch names indicate what evidence is available. Each branch proves the same goal R.

For nested case splits, avoid excessive nesting when possible. Extract helper lemmas if the branches become long.

Use `have` for Named Intermediate Facts

The have command adds a local theorem to the context.

theorem have_example
    (P Q R S : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hRS : R -> S)
    (hp : P) :
    S := by
  have hq : Q := hPQ hp
  have hr : R := hQR hq
  have hs : S := hRS hr
  exact hs

A good have statement should have a type that explains why it exists. If the type is obscure, the proof will be obscure.

Use Anonymous `have` Sparingly

Lean allows unnamed intermediate facts:

theorem anonymous_have
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  have : Q := hPQ hp
  exact hQR this

This is acceptable when there is only one unnamed fact in scope. In longer proofs, named facts are safer.

Use `suffices` to State the Missing Step

The suffices command changes the proof into a named subgoal that is enough to prove the target.

theorem suffices_example
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  suffices hq : Q from hQR hq
  exact hPQ hp

This reads as: it is enough to prove Q, because Q implies R.

Use suffices when the intermediate claim is conceptually prior to the final conclusion.

Use `show` to Clarify the Current Goal

The show command states what the current goal should be.

theorem show_example
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  constructor
  · show P
    exact hp
  · show Q
    exact hq

This is useful when the goal has been simplified or rewritten and is no longer visually obvious.

Separate Proof Search from Proof Shape

Automation is useful, but it should not hide the main argument.

theorem automation_local
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  constructor
  · exact hp
  · exact hq

This proof is better than:

theorem automation_too_much
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  aesop

The aesop version is shorter, but it hides the introduction rule for conjunction. Use broad automation when the logical structure is routine or irrelevant to the section.

Structure Rewriting Proofs

For equality proofs, prefer a calc block when the chain matters.

theorem calc_structure
    (a b c d : Nat)
    (hAB : a = b)
    (hBC : b = c)
    (hCD : c = d) :
    a = d := by
  calc
    a = b := hAB
    _ = c := hBC
    _ = d := hCD

Use rw when the rewrite is local and obvious.

theorem rw_structure
    (a b : Nat)
    (h : a = b) :
    a + 1 = b + 1 := by
  rw [h]

Use Helper Lemmas

If a proof repeats the same local pattern, extract a lemma.

theorem imp_trans
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R) :
    P -> R := by
  intro hp
  exact hQR (hPQ hp)

Then use it:

theorem helper_lemma_example
    (P Q R S : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hRS : R -> S)
    (hp : P) :
    S := by
  exact hRS (imp_trans P Q R hPQ hQR hp)

The helper lemma gives a reusable name to a common reasoning step.

Prefer Stable Proofs

A proof is stable if small changes to definitions do not break unrelated parts.

Stable proofs usually:

name important intermediate facts
avoid relying on fragile context order
keep automation local
use explicit rewrite rules
avoid unnecessary unfolding

For example:

theorem stable_rewrite
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  rw [hAB]
  simp

This says exactly which equality is used, then lets simp handle the standard arithmetic cleanup.

Common Patterns

Use this skeleton for implication-heavy proofs:

theorem skeleton
    (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hPQ hQR hp
  have hq : Q := hPQ hp
  exact hQR hq

Use this skeleton for conjunction-heavy proofs:

theorem conjunction_skeleton
    (P Q R : Prop)
    (h : P ∧ Q)
    (hQR : Q -> R) :
    P ∧ R := by
  rcases h with ⟨hp, hq⟩
  have hr : R := hQR hq
  exact ⟨hp, hr⟩

Use this skeleton for disjunction-heavy proofs:

theorem disjunction_skeleton
    (P Q R : Prop)
    (h : P ∨ Q)
    (hPR : P -> R)
    (hQR : Q -> R) :
    R := by
  cases h with
  | inl hp =>
    exact hPR hp
  | inr hq =>
    exact hQR hq

Common Pitfalls

Do not compress a proof before it is understood. First write the explicit proof, then shorten only the parts that remain obvious.

Do not leave important intermediate claims unnamed. If a fact has mathematical meaning, give it a name.

Do not use broad automation to hide the connective being introduced or eliminated in a beginner proof.

Do not destructure hypotheses far away from where they are introduced unless delaying the destructuring improves readability.

Do not let branch proofs drift into different styles unless the cases are genuinely different.

Takeaway

Proof structure is part of the proof. Introduce assumptions first, unpack compound data early, name important intermediate facts, and build the final goal explicitly. Use compact terms and automation only where they preserve the shape of the argument.