Proof Workflow

Learn a repeatable process for building proofs: read the goal, introduce assumptions, simplify, and close with a finishing tactic.

Read the Goal First

Every proof starts with a goal. Before choosing a tactic, identify the shape of the goal and what it expects. The goal appears after the ⊢symbol in the Infoview. Understanding the goal's structure—whether it's an implication, a universal statement, an equality, or a conjunction—determines which tactic to use.

Common goal shapes and their meanings:

• P → Q: An implication—assume P, prove Q
• ∀ x, P x: A universal—prove P for an arbitrary x
• a = b: An equality—show both sides are the same
• P ∧ Q: A conjunction—prove both P and Q
• P ∨ Q: A disjunction—prove at least one of P or Q

1example : Nat → Nat := by
2  -- Goal: Nat → Nat
3  -- This is a function type, so we introduce the input
4  intro n
5  -- Goal: Nat
6  -- Now we just need to produce a Nat
7  exact n + 1

The Infoview updates after each tactic, showing how the goal changes. Watch it like a debugging panel—it tells you exactly what remains to prove.

Introduce, Then Simplify

Most goals become easier once you move assumptions into context and simplify the target. The general strategy is: first use intro to bring universals and implications into your hypothesis list, then use simp orrw to clean up the goal.

This "introduce then simplify" pattern handles the majority of proofs:

1-- Simple simplification
2example (n : Nat) : n + 0 = n := by
3  simp  -- simp knows n + 0 = n
4
5-- Reflexivity when both sides are identical
6example (n : Nat) : n = n := by
7  rfl  -- Both sides compute to the same thing

When you have hypotheses available, include them in your simplification:

1example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
2  simp [h]  -- Uses h to rewrite a to b, then simplifies
3
4example (n : Nat) (h : n = 5) : n + 0 = 5 := by
5  simp only [Nat.add_zero, h]  -- Explicit about which lemmas

Close with a Finisher

If the goal is exactly a hypothesis, use exact orassumption. If it’s a definitional equality, try rfl. These "finisher" tactics close the proof when only the final step remains.

exact requires you to specify exactly which term proves the goal.assumption searches your hypotheses automatically. Useexact when you know what you need; use assumptionwhen the answer is obviously in scope.

1-- exact: specify the proof term
2example (P Q : Prop) (hp : P) : P := by
3  exact hp
4
5-- assumption: auto-search hypotheses
6example (P Q : Prop) (hp : P) (hq : Q) : P := by
7  assumption  -- Finds hp automatically
8
9-- rfl: definitional equality
10example : (2 : Nat) = 2 := by
11  rfl
12
13-- trivial: handles True and similar goals
14example : True := by
15  trivial

If none of these work, your goal likely needs further transformation. Go back to simplification or try rewriting with rw.

Pick the Right Tactic

A fast workflow is about choosing the simplest tactic that moves the goal forward. Here's a quick reference for common goal shapes:

When in doubt, try simp first. It often cleans up the goal enough that the next step becomes obvious.

Debugging Stuck Proofs

Even experienced users get stuck. Here's how to diagnose and fix common issues:

Check the Goal Carefully

Sometimes the goal looks right but has subtle differences—like implicit arguments or different universes. Hover over terms in the Infoview to see their full types.

Use simp? and exact?

These "?" tactics suggest what to use:

1example (n : Nat) : n + 0 = n := by
2  simp?
3  -- Try this:
4  --   [apply] simp only [Nat.add_zero]
5
6example (P : Prop) (hp : P) : P := by
7  exact?  -- Try this: exact hp

Prove the Goal Backwards

Do not be afraid to write a proof skeleton full of sorryand fill it in afterwards. Lean will typecheck the structure and tell you the exact goal at each hole — which is often the information you were missing.

1example (a b : Nat) (h : a ≤ b) : a * 2 ≤ b * 2 := by
2  have step1 : a + a ≤ b + b := by sorry   -- fill in later
3  have step2 : a * 2 = a + a := by sorry
4  sorry
5-- Each sorry shows you a concrete, smaller goal in the Infoview.
6-- Replace them one at a time; the structure is already checked.

Break Complex Goals Apart

If the goal is overwhelming, use have to prove intermediate steps:

1example (xs ys : List Nat) (h : xs = ys) : xs.length + 1 = ys.length + 1 := by
2  -- Prove the small fact first, give it a name...
3  have hlen : xs.length = ys.length := by rw [h]
4  -- ...then the main goal follows from it
5  rw [hlen]
6
7-- have is also how you introduce a fact the goal does not mention:
8example (n : Nat) (h : n > 3) : n * 2 > 6 := by
9  have h4 : n ≥ 4 := h
10  omega

1example (P Q : Prop) : P → Q → P := by
2  intro hp hq
3  exact hp

1example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
2  constructor
3  · exact hp
4  · exact hq