1.6 Theorems with `theorem` and `lemma`

Lean treats a theorem as a named proof. The name is stored in the environment, the statement is its type, and the proof is the term assigned to that type. This is the same basic mechanism used by def, but the type of a theorem is a proposition.

Problem

You want to state mathematical facts, prove them, reuse them later, and understand the practical difference between theorem, lemma, and def.

Solution

Use theorem or lemma to introduce a named proof.

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

This theorem says that every proposition implies itself. The parameter P : Prop is arbitrary. After introducing a hypothesis h : P, the goal is exactly P, so exact h finishes the proof.

You can check the theorem:

#check id_prop

Lean reports:

id_prop : (P : Prop) -> P -> P

Theorem Shape

The general form is:

theorem name (parameters) : proposition :=
  proof

A tactic proof uses by:

theorem true_intro_example : True := by
  trivial

A term proof gives the proof object directly:

theorem true_intro_example_term : True :=
  True.intro

Both forms create a declaration whose type is a proposition.

Lemma Shape

In Lean, lemma is practically the same kind of declaration as theorem.

lemma and_left (P Q : Prop) : P -> Q -> P := by
  intro hp hq
  exact hp

The usual convention is stylistic:

Lean checks all three using the same kernel discipline.

Examples Without Names

Use example for exploration:

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

An example is checked but does not create a reusable global name. It is useful in a cookbook recipe, a scratch file, or a local proof experiment.

Assumptions as Parameters

A theorem can take propositions and proofs as parameters.

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

Here hpq : P -> Q is a proof that P implies Q, and hp : P is a proof of P. Applying hpq to hp produces a proof of Q.

The same proof can be written more compactly:

theorem modus_ponens_term (P Q : Prop) (hp : P) (hpq : P -> Q) : Q :=
  hpq hp

Local Intermediate Results

Use have to create an intermediate proof.

theorem chain_implication (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) : P -> R := by
  intro hp
  have hq : Q := hpq hp
  have hr : R := hqr hq
  exact hr

This pattern is useful when a proof has several logical steps. The local names hq and hr make the data flow explicit.

Equality Theorems

The simplest equality proof is rfl.

theorem add_zero_example : 0 + 3 = 3 := by
  rfl

For many arithmetic expressions, simplification is clearer:

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

The first theorem works by computation. The second uses the simplifier and library facts about natural-number addition.

Reusing Theorems

Once named, a theorem can be applied like a function.

theorem use_id_prop (P : Prop) (hp : P) : P := by
  exact id_prop P hp

Because the proposition P can often be inferred, this can also be written:

theorem use_id_prop_inferred (P : Prop) (hp : P) : P := by
  exact id_prop P hp

For implicit arguments, a theorem can be designed like this:

theorem id_prop_implicit {P : Prop} : P -> P := by
  intro h
  exact h

theorem use_id_prop_implicit (P : Prop) (hp : P) : P := by
  exact id_prop_implicit hp

Implicit parameters make reuse less noisy.

Theorems Are Terms

A theorem has a type and can be passed around.

#check id_prop
#check id_prop True

The expression:

id_prop True

has type:

True -> True

This is ordinary function application. A proof of implication is a function from proofs of the premise to proofs of the conclusion.

by Blocks

A by block switches into tactic mode.

theorem and_comm_example (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  constructor
  · exact h.right
  · exact h.left

The tactic script transforms the initial goal into smaller goals. The bullets separate the two subgoals produced by constructor.

Term-Mode Version

The same theorem can be written as a term:

theorem and_comm_example_term (P Q : Prop) : P ∧ Q -> Q ∧ P :=
  fun h => And.intro h.right h.left

Term mode is often shorter when the proof object is simple. Tactic mode is often clearer when the proof needs several transformations.

Theorem Names

Names should describe the statement, not the proof script.

Good names:

and_comm
imp_trans
map_id
append_nil

Poor names:

proof1
thing
easy
works

A theorem name becomes part of the searchable interface of a project. In a large library, name quality directly affects reuse.

Attributes on Theorems

A theorem can be marked for automation.

@[simp]
theorem id_apply {α : Type} (x : α) : id x = x := by
  rfl

The attribute [simp] registers the theorem as a simplification rule. After that, simp may use it automatically.

Use such attributes carefully. A bad simp theorem can make proofs slower or cause rewriting loops.

Common Pitfalls

If exact h fails, the type of h does not match the goal. Use #check h in term mode, or inspect the goal state in the editor.

If apply creates unexpected goals, the theorem being applied has premises that must still be proved.

If simp does nothing, the needed theorem may not be in the simp set, or the expression may not match the theorem shape.

If a theorem is hard to reuse, consider making some parameters implicit.

If a proof becomes long, introduce intermediate facts with have.

Takeaway

theorem and lemma introduce reusable proofs. A theorem statement is a type in Prop, and the proof is a term of that type. Tactic mode and term mode are two ways to construct the same object. Good theorem design means clear statements, reusable parameters, stable names, and controlled automation attributes.