Proof Strategy

The previous articles taught you individual tactics. Now we learn how to think. A proof is not a random sequence of tactics that happens to work. It is a structured argument, and understanding that structure makes the difference between flailing and fluency. The gap between knowing the tactics and knowing how to prove things is the gap between knowing the rules of chess and knowing how to not lose immediately.

The Goal State

Every proof begins with a goal and ends with no goals. The goal state is your map. Learning to read it fluently is the most important skill in tactic-based proving.

case succ
n : Nat
ih : P n
⊢ P (n + 1)

This goal state tells you everything: you are in the succ case of an induction, you have a natural number n, you have an induction hypothesis ih stating that P n holds, and you must prove P (n + 1). The turnstile ⊢ separates what you have from what you need.

When a proof has multiple goals, they appear stacked. The first goal is your current focus. Tactics typically operate on the first goal, though combinators like all_goals and any_goals can target multiple goals simultaneously.

Categories of Tactics

Tactics fall into natural categories based on what they do to the goal state. Understanding these categories helps you choose the right tool.

Introduction tactics move structure from the goal into the context. When your goal is P → Q, the tactic intro h assumes P (calling it h) and changes the goal to Q. When your goal is ∀ x, P x, the tactic intro x introduces a fresh x and changes the goal to P x. Introduction tactics make progress by assuming what you need to prove under.

Elimination tactics use structure from the context to transform the goal. When you have h : P ∧ Q and need P, the tactic exact h.1 extracts the left component. When you have h : P ∨ Q, the tactic cases h splits into two goals, one assuming P and one assuming Q. Elimination tactics make progress by using what you have.

Rewriting tactics transform the goal using equalities. The tactic rw [h] replaces occurrences of the left side of h with the right side. The tactic simp applies many such rewrites automatically. Rewriting makes progress by simplifying toward something obviously true.

Automation tactics search for proofs. The tactic simp tries simplification lemmas. The tactic omega solves linear arithmetic. The tactic aesop performs general proof search. Automation makes progress by doing work you would rather not do by hand.

Structural tactics manipulate the proof state without making logical progress. The tactic swap reorders goals. The tactic rename changes hypothesis names. The tactic clear removes unused hypotheses. These tactics keep your proof organized.

Reading the Goal

Before applying any tactic, ask: what is the shape of my goal?

Implication (P → Q): Use intro to assume P and prove Q.

Universal (∀ x, P x): Use intro x to introduce x and prove P x.

Conjunction (P ∧ Q): Use constructor to split into two goals, one for P and one for Q. Or use And.intro directly.

Disjunction (P ∨ Q): Use left to commit to proving P, or right to commit to proving Q.

Existential (∃ x, P x): Use use t to provide a witness t and prove P t.

Equality (a = b): Try rfl if definitionally equal. Try simp for simplification. Try rw with known equalities. Try ring for algebraic identities.

Negation (¬P): Remember that ¬P is P → False. Use intro h to assume P and derive a contradiction.

False: If your goal is False, you need a contradiction. Look for hypotheses that conflict.

Reading the Context

Your context contains hypotheses. Each hypothesis is a tool. Ask: what can I do with each hypothesis?

Implication (h : P → Q): If you can prove P, you can get Q. Use apply h when your goal is Q. Use have hq := h hp when you have hp : P.

Universal (h : ∀ x, P x): You can instantiate at any term. Use specialize h t to get P t. Use have ht := h t to keep the original.

Conjunction (h : P ∧ Q): You have both P and Q. Access them with h.1 and h.2, or use obtain ⟨hp, hq⟩ := h to destructure.

Disjunction (h : P ∨ Q): You have either P or Q but do not know which. Use cases h to split into cases.

Existential (h : ∃ x, P x): There is some x satisfying P. Use obtain ⟨x, hx⟩ := h to get the witness and its property.

Equality (h : a = b): You can substitute b for a. Use rw [h] to rewrite left-to-right. Use rw [← h] to rewrite right-to-left.

Proof Patterns

Certain proof structures recur constantly. Recognizing them saves time.

Direct proof: Introduce assumptions, manipulate, conclude. Most proofs follow this pattern.

theorem direct (P Q : Prop) (h : P → Q) (hp : P) : Q := by
  apply h
  exact hp

Proof by cases: When you have a disjunction or an inductive type, split and prove each case.

theorem by_cases (n : Nat) : n = 0 ∨ n ≥ 1 := by
  cases n with
  | zero => left; rfl
  | succ m => right; simp

Proof by induction: For properties of recursive types, prove the base case and the inductive step.

theorem by_induction (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [ih]

Proof by contradiction: Assume the negation and derive False.

theorem by_contradiction (P : Prop) (h : ¬¬P) : P := by
  by_contra hnp
  exact h hnp

Proof by contraposition: To prove P → Q, prove ¬Q → ¬P instead.

theorem by_contraposition (P Q : Prop) (h : ¬Q → ¬P) : P → Q := by
  intro hp
  by_contra hnq
  exact h hnq hp

When You Get Stuck

Every proof hits obstacles. Here is how to get unstuck.

Simplify first. Try simp or simp only [relevant_lemmas]. Often the goal simplifies to something obvious.

Check your hypotheses. Do you have what you need? Use have to derive intermediate facts. Use obtain to destructure complex hypotheses.

Try automation. For arithmetic, try omega or linarith. For algebraic identities, try ring or field_simp. For general goals, try aesop or decide.

Work backwards. What would make your goal obviously true? If you need P ∧ Q, you need to prove both P and Q. What tactics produce those subgoals?

Work forwards. What can you derive from your hypotheses? If you have h : P → Q and hp : P, you can derive Q.

Split the problem. Use have to state and prove intermediate lemmas. Breaking a proof into steps often reveals the path.

Read the error. Lean’s error messages are verbose but precise. “Type mismatch” tells you what was expected and what you provided. “Unknown identifier” means a name is not in scope. “Unsolved goals” means you are not done.

Use the library. Mathlib contains thousands of lemmas. Use exact? to search for lemmas that close your goal. Use apply? to search for lemmas whose conclusion matches your goal.

Tactic Composition

Tactics compose in several ways.

Sequencing: Separate tactics with newlines or semicolons. Each tactic operates on the result of the previous one.

theorem seq_demo (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  constructor
  exact h.2
  exact h.1

Focusing: Use · to focus on a single goal. Indentation groups tactics under a focus.

theorem focus_demo (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  constructor
  · exact h.2
  · exact h.1

Combinators: Use <;> to apply a tactic to all goals produced by the previous tactic. Use first | t1 | t2 to try tactics in order. Use repeat t to apply a tactic until it fails.

theorem combinator_demo (P : Prop) (h : P) : P ∧ P ∧ P := by
  constructor <;> (try constructor) <;> exact h

Next-Generation Automation

The tactics described so far require you to think. You read the goal, choose a strategy, apply tactics step by step. This is how mathematicians have always worked, and there is value in understanding your proof at every stage. But a new generation of tactics is changing the calculus of what is worth formalizing.

Higher-order tactics like aesop, grind, and SMT integration lift proof development from low-level term manipulation to structured, automated search over rich proof states. Instead of specifying every proof step, you specify goals, rule sets, or search parameters, and these tactics synthesize proof terms that Lean’s kernel then checks. The soundness guarantee remains absolute since the kernel verifies everything, but the human cost drops dramatically. This decoupling of “what should be proved” from “how to construct the term” is what makes large-scale formalization feasible.

aesop implements white-box best-first proof search, exploring a tree of proof states guided by user-configurable rules. Unlike black-box automation, aesop lets you understand and tune the search: rules are indexed via discrimination trees for rapid retrieval, and you can register domain-specific lemmas to teach it new tricks. grind draws inspiration from modern SMT solvers, maintaining a shared workspace where congruence closure, E-matching, and forward chaining cooperate on a goal. It excels when many interacting equalities and logical facts are present, automatically deriving consequences that would be tedious to script by hand. For goals requiring industrial-strength decision procedures, SMT tactics send suitable fragments to proof-producing solvers like cvc5, then reconstruct proofs inside Lean so the kernel can verify them. This lets Lean leverage decades of solver engineering while preserving the LCF-style trust model where only the small kernel must be trusted.

The strategic question is when to reach for automation versus working by hand. The temptation is to try grind on everything and move on when it works. This is efficient but opaque: you learn nothing, and when automation fails on a similar goal later, you have no insight into why. A better approach is to use automation to explore, then understand what it found. Goals that would take an hour of tedious case analysis now take seconds. This frees you to tackle harder problems. But remember: when grind closes a goal, it has found a valid proof term. It has not gained insight. That remains your job.

What Comes Next

The following article is a reference. It documents every major tactic in Lean 4 and Mathlib, organized alphabetically. You do not need to memorize it. You need to know it exists, and you need to know how to find the tactic you need.

When you encounter a goal you do not know how to prove, return here. Ask: what is the shape of my goal? What is in my context? What pattern does this proof follow? The answer will point you to the right tactic, and the reference will tell you how to use it.

The strategies in this article apply beyond Lean. The structure of mathematical argument is universal. Direct proof, case analysis, induction, contradiction: these are the fundamental patterns of reason itself. Learning them in a proof assistant merely makes them explicit. You cannot handwave past a case you forgot to consider when the computer is watching.