# 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.

```lean id="1ncs9z"
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:

```lean id="vf1d29"
#check id_prop
```

Lean reports:

```text id="ixb8wk"
id_prop : (P : Prop) -> P -> P
```

## Theorem Shape

The general form is:

```lean id="vxvi30"
theorem name (parameters) : proposition :=
  proof
```

A tactic proof uses `by`:

```lean id="mgw2d9"
theorem true_intro_example : True := by
  trivial
```

A term proof gives the proof object directly:

```lean id="etjgme"
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`.

```lean id="x1304n"
lemma and_left (P Q : Prop) : P -> Q -> P := by
  intro hp hq
  exact hp
```

The usual convention is stylistic:

| Keyword   | Usual role                             |
| --------- | -------------------------------------- |
| `lemma`   | Supporting result used by later proofs |
| `theorem` | Main named result                      |
| `example` | Temporary or unnamed proof             |

Lean checks all three using the same kernel discipline.

## Examples Without Names

Use `example` for exploration:

```lean id="j8pc4p"
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.

```lean id="c25d1n"
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:

```lean id="618gmp"
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.

```lean id="spc9pz"
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`.

```lean id="4x217y"
theorem add_zero_example : 0 + 3 = 3 := by
  rfl
```

For many arithmetic expressions, simplification is clearer:

```lean id="85rv6n"
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.

```lean id="mmpw3y"
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:

```lean id="ydar8l"
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:

```lean id="zl271a"
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.

```lean id="1ac9br"
#check id_prop
#check id_prop True
```

The expression:

```lean id="6sqi2u"
id_prop True
```

has type:

```text id="z8x1fa"
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.

```lean id="gpby0w"
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:

```lean id="cyrjeh"
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:

```lean id="qk84pv"
and_comm
imp_trans
map_id
append_nil
```

Poor names:

```lean id="bvw7ns"
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.

```lean id="42hocn"
@[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.