The Proof State

When you enter tactic mode, Lean shows you the "proof state"—what you have and what you need to prove. Learning to read it is essential.

Entering Tactic Mode

Use by to switch from writing terms to writing tactics:

1-- Term mode: write the proof directly
2example : 2 + 2 = 4 := rfl
3
4-- Tactic mode: build the proof step by step
5example : 2 + 2 = 4 := by
6  rfl

In your editor (with the Lean extension), placing your cursor after byshows the proof state in the Infoview panel.

Reading the Proof State

The proof state has two parts:

1-- Hypotheses (what you have)
2a : Nat
3b : Nat
4h : a = b
5⊢ b = a      -- Goal (what you need to prove)

• Above the ⊢: Your hypotheses (assumptions you can use)
• After the ⊢: Your goal (what you need to prove)

The turnstile ⊢ (typed as \vdash) separates what you have from what you need.

Goals and Subgoals

Some tactics split one goal into multiple subgoals:

1example : True ∧ True := by
2  constructor
3  -- Now we have TWO goals:
4  -- case left:  ⊢ True
5  -- case right: ⊢ True
6  · trivial   -- Solve first goal
7  · trivial   -- Solve second goal

The · (bullet) focuses on one goal at a time. You can also use braces or indentation:

1example : True ∧ True := by
2  constructor
3  { trivial }  -- First goal
4  { trivial }  -- Second goal
5
6-- Or just chain them (when order is unambiguous)
7example : True ∧ True := by
8  constructor <;> trivial  -- Apply trivial to all goals

Watching the State Change

Each tactic transforms the proof state. Watch how it evolves:

1example (a b : Nat) : a + b = b + a := by
2  -- State: a b : Nat ⊢ a + b = b + a
3  
4  rw [Nat.add_comm]
5  -- State: a b : Nat ⊢ b + a = b + a
6  
7  rfl
8  -- No goals! Proof complete.

Common Proof State Patterns

Simple Goal

1⊢ 2 + 2 = 4

No hypotheses, just need to prove the goal directly.

Goal with Hypotheses

1n : Nat
2h : n > 0
3⊢ n ≠ 0

You have a natural number n and know it's positive. Use this to prove it's not zero.

Function to Prove (→)

1⊢ a = b → b = a

Use intro to assume a = band prove b = a.

Universal Statement (∀)

1⊢ ∀ n : Nat, n + 0 = n

Use intro n to fix an arbitrary nand prove the property for it.

The Infoview Panel

In VS Code with the Lean 4 extension, the Infoview panel (usually on the right) shows:

• The current proof state at your cursor position
• Type information for expressions
• Error messages and suggestions
• Documentation for tactics and lemmas

Interactive Example

1-- Try stepping through this proof in your editor
2theorem symmetry (a b : Nat) (h : a = b) : b = a := by
3  -- Cursor here:
4  -- a b : Nat
5  -- h : a = b
6  -- ⊢ b = a
7  
8  rw [h]
9  -- Cursor here:
10  -- a b : Nat
11  -- h : a = b
12  -- ⊢ a = a
13  
14  rfl
15  -- No goals

1example : P := by tactic1; tactic2; tactic3

1theorem myThm : 2 + 2 = 4 := by rfl
2
3#print myThm  -- Shows: theorem myThm : 2 + 2 = 4 := rfl

Proof Complete

When no goals remain, the proof state shows:

1No goals

or simply nothing. At this point, Lean has verified your proof is complete and correct.