1.18 Basic Tactic Mode

Tactic mode is an interactive way to build proofs. Instead of writing a proof term directly, you write commands that transform the current goal into simpler goals. Lean checks that the final result is still a proof term of the required proposition.

Problem

You want to prove simple propositions by inspecting the goal, introducing assumptions, applying known facts, and closing goals step by step.

Solution

Use by to enter tactic mode.

theorem identity_example (P : Prop) : P -> P := by
  intro h
  exact h

The theorem states that every proposition implies itself. After intro h, the local context contains:

P : Prop
h : P

and the goal is:

P

The tactic exact h closes the goal because h has exactly the required type.

Goals

A goal is the proposition Lean still needs to prove. In tactic mode, the editor displays the current goal and local context.

For example:

theorem example_goal (P Q : Prop) : P -> Q -> P := by
  intro hp
  intro hq
  exact hp

After the two introductions, the context contains:

P Q : Prop
hp : P
hq : Q

and the goal is:

P

The proof closes with hp.

intro

The intro tactic introduces a hypothesis or parameter.

theorem imp_chain (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hpq
  intro hqr
  intro hp
  exact hqr (hpq hp)

Each intro removes one leading implication or universal quantifier from the goal and adds a named object to the context.

exact

The exact tactic closes the goal with a term whose type matches the goal.

theorem exact_example (P : Prop) (h : P) : P := by
  exact h

If the goal is P, then exact h succeeds precisely when h : P.

apply

The apply tactic uses a theorem or function backward.

theorem apply_example (P Q : Prop) (hpq : P -> Q) (hp : P) : Q := by
  apply hpq
  exact hp

After apply hpq, Lean changes the goal from Q to P, because hpq can prove Q if given a proof of P.

This is backward reasoning: choose a rule that can prove the current goal, then prove its premises.

assumption

The assumption tactic searches the local context for a hypothesis that matches the goal.

theorem assumption_example (P : Prop) (h : P) : P := by
  assumption

This succeeds because h : P is already available.

Use assumption when the goal is directly present in the context.

constructor

The constructor tactic splits goals whose proof is built by a constructor.

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

The goal P ∧ Q becomes two goals:

P
Q

The bullets mark the separate subproofs.

cases

The cases tactic performs case analysis on data or proofs.

theorem and_elim_left (P Q : Prop) (h : P ∧ Q) : P := by
  cases h with
  | intro hp hq =>
      exact hp

A proof of P ∧ Q contains a proof of P and a proof of Q. The cases tactic exposes both components.

For disjunction:

theorem or_comm_example (P Q : Prop) : P ∨ Q -> Q ∨ P := by
  intro h
  cases h with
  | inl hp =>
      right
      exact hp
  | inr hq =>
      left
      exact hq

Each branch handles one constructor of the disjunction.

left and right

The tactics left and right choose a side of a disjunction.

theorem left_example (P Q : Prop) (hp : P) : P ∨ Q := by
  left
  exact hp

theorem right_example (P Q : Prop) (hq : Q) : P ∨ Q := by
  right
  exact hq

Use these when the goal is an Or.

have

The have tactic creates an intermediate fact.

theorem have_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 makes the proof readable by naming each step.

show

The show tactic changes the displayed goal to an equivalent target.

theorem show_example (P : Prop) (h : P) : P := by
  show P
  exact h

In simple examples this looks redundant, but it is useful when Lean displays a reducible expression and you want to state the intended goal explicitly.

rw

The rw tactic rewrites using equalities.

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

The equality h : a = b replaces a with b.

simp

The simp tactic simplifies expressions using definitional reduction and registered simplification lemmas.

theorem simp_example (n : Nat) : n + 0 = n := by
  simp

Use simp for standard simplifications. Use rw when you want a specific rewrite.

Combining Tactics

A proof often combines several small tactics.

theorem combined_example (P Q R : Prop)
    (hp : P) (hq : Q) : (P ∧ Q) ∨ R := by
  left
  constructor
  · exact hp
  · exact hq

This proof first chooses the left side of the disjunction, then constructs the conjunction.

Tactic Blocks Produce Terms

A tactic proof is still a term.

theorem tactic_term_example (P : Prop) : P -> P := by
  intro h
  exact h

The corresponding term proof is:

theorem term_example (P : Prop) : P -> P :=
  fun h => h

Both declarations have the same type:

#check tactic_term_example
#check term_example

Common Pitfalls

If exact h fails, check whether the type of h exactly matches the goal.

If apply f creates unexpected goals, inspect the type of f.

If constructor creates several goals, use bullets to keep them separated.

If cases h removes a hypothesis, remember that it replaces the original object with its constructor fields.

If simp closes too much or changes the goal unexpectedly, use rw for more control.

Recipe: Prove by Goal Reduction

Start with the goal:

theorem recipe (P Q : Prop) : P -> Q -> P ∧ Q := by

Introduce assumptions:

  intro hp
  intro hq

Split the conjunction:

  constructor

Solve each subgoal:

  · exact hp
  · exact hq

Full proof:

theorem recipe (P Q : Prop) : P -> Q -> P ∧ Q := by
  intro hp
  intro hq
  constructor
  · exact hp
  · exact hq

Takeaway

Tactic mode is a controlled proof construction process. Each tactic transforms the current goal or uses information from the context. Basic tactics such as intro, exact, apply, constructor, cases, rw, and simp are enough to write many small proofs and to understand the shape of larger ones.