Introduction and elimination in Lean

A Lean proof is a conversation between two lists: the assumptions we may use and the goal we must prove. The outermost logical operator tells us what to try next.

This is the same viewpoint developed in Section 1.1 of Clive Newstead's An Infinite Descent into Pure Mathematics. An introduction rule explains how to prove a proposition containing an operator; an elimination rule explains how to use an assumption containing that operator. Lean makes those two moves visible.

Operator	To prove it: introduction	To use it: elimination
`P ∧ Q`	Prove `P` and prove `Q`.	Extract a proof of `P` and a proof of `Q`.
`P → Q`	Assume `P`, then prove `Q`.	Combine `P → Q` with a proof of `P` to obtain `Q`.
`P ↔ Q`	Prove both `P → Q` and `Q → P`.	Use either direction: obtain `Q` from `P`, or `P` from `Q`.
`P ∨ Q`	Prove either `P` or `Q`.	Argue by cases: derive the same conclusion first from `P`, then from `Q`.
`¬ P`	Assume `P`, then derive a contradiction.	Combine `¬ P` with a proof of `P` to obtain a contradiction.

Setup for the web editor

The Lean web editor cannot import our local macros.lean file. Copy the entire block below to the top of the editor instead. It defines the readable tactics used in these examples and declares P, Q, R, and S to be propositions.

macro "conj_elim" hp:ident hq:ident "from" h:ident : tactic =>
  `(tactic|(apply And.elim _ $h; intro $hp $hq))

macro "conj_intro" h:ident "from" hp:ident hq:ident : tactic =>
  `(tactic|(have $h : _∧_ := And.intro $hp $hq))

macro "disj_elim" hp:ident hq:ident "from" h:term:arg : tactic =>
  `(tactic|(refine Or.elim $h (fun $hp => ?_) (fun $hq => ?_)))

macro "disj_intro_left" h:ident "from" hp:ident q:term:arg : tactic =>
  `(tactic|(have $h : _∨($q) := Or.inl $hp))

macro "disj_intro_right" h:ident "from" p:term:arg hq:ident : tactic =>
  `(tactic|(have $h : ($p)∨_ := Or.inr $hq))

macro "impl_elim" hq:ident "from" hp:ident hpq:ident : tactic =>
  `(tactic|(have $hq := $hpq $hp))

variable (P Q R S : Prop)

Typing logical symbols

Lean source uses symbols such as ∧ and →, but you do not need to find them in a character picker. In the Lean editor, type a backslash command and then press Space (or Tab) to complete it.

Type	Lean inserts	Meaning	Example
`\and`	`∧`	and	`P ∧ Q`
`\or`	`∨`	or	`P ∨ Q`
`\to`	`→`	implies	`P → Q`
`\neg`	`¬`	not	`¬ P`
`\iff`	`↔`	if and only if	`P ↔ Q`
`\forall`	`∀`	for every	`∀ x, P`
`\exists`	`∃`	there exists	`∃ x, P`

For example, typing P \and Q \to R and completing each command produces P ∧ Q → R. Use parentheses whenever they make the intended logical structure clearer. The worked proofs below use conjunction, implication, disjunction, and negation.

First, read the proof state

After Lean enters proof mode at by, it displays assumptions above a turnstile and the current goal below it. For

example (h : P ∧ Q) : Q ∧ P := by

we may read the state schematically as

h : P ∧ Q
⊢ Q ∧ P

The assumption begins with a conjunction, so it can be eliminated. The goal begins with a conjunction, so it can be introduced. That observation is already a proof plan.

Keep an unfinished goal visible

In the web editor, pressing Enter after a tactic moves the cursor onto a position that does not yet contain a tactic. The Tactic state panel may become empty even though the goal is still present; the unfinished goal then appears in All Messages. To keep the current goal visible while building a proof, leave a sorry placeholder after the tactics you have written and put the cursor on sorry.

case inl hp =>
  apply Or.intro_right
  sorry  -- Keep this placeholder until the branch is complete.

Here apply Or.intro_right changes the goal from Q ∨ P to P. Putting the cursor on sorry displays that goal. Replace sorry with exact hp when you are ready to finish the branch.

Conjunction: “and”

Proving P ∧ Q: prove both parts.

Assuming P ∧ Q: use each part separately.

Use a conjunction: `conj_elim`

The command conj_elim hp hq from h takes apart h : P ∧ Q. It adds two new facts, hp : P and hq : Q, to our assumptions.

Build a conjunction: `conj_intro`

If we already have proofs of both parts, conj_intro hqp from hq hp combines them and names the resulting proof hqp. Finally, exact hqp closes the goal because hqp has exactly the required type.

example (h : P ∧ Q) : Q ∧ P := by
  conj_elim hp hq from h
  conj_intro hqp from hq hp
  exact hqp

This proof increases our stock of known facts until one of them matches the goal. The two custom commands are readable names for conjunction elimination and introduction; they are defined in macros.lean using Lean's underlying rules.

Let the goal lead: `apply And.intro`

We can instead work backward from the goal. Applying the conjunction introduction rule to the goal Q ∧ P replaces it with two smaller goals, first Q and then P.

example (h : P ∧ Q) : Q ∧ P := by
  conj_elim hp hq from h
  apply And.intro
  exact hq
  exact hp

In textbook language, apply And.intro implements Strategy 1.1.7, proving conjunctions, while conj_elim implements Strategy 1.1.9, assuming conjunctions.

Parentheses are logical structure

Conjunctions nest. The expression P ∧ Q ∧ R is read as P ∧ (Q ∧ R), so we eliminate it twice. The goal (P ∧ Q) ∧ R also contains two conjunctions, so we introduce twice.

example (h : P ∧ Q ∧ R) : (P ∧ Q) ∧ R := by
  conj_elim hp hqr from h
  conj_elim hq hr from hqr
  apply And.intro
  apply And.intro
  exact hp
  exact hq
  exact hr

Implication: “if … then …”

Proving P → Q: assume P and prove Q.

Assuming P → Q: give it a proof of P to obtain a proof of Q.

Prove an implication: `intro`

If the goal is P → R, intro hp follows the implication introduction rule: it temporarily assumes P, names that assumption hp, and leaves R as the new goal.

Use an implication: `impl_elim`

If hpq : P → Q and hp : P, then impl_elim hq from hp hpq deduces and names hq : Q. This is implication elimination, also called modus ponens in Section 1.1.

example (hpq : P → Q) (hqr : Q → R) : P → R := by
  intro hp
  impl_elim hq from hp hpq
  impl_elim hr from hq hqr
  exact hr

Here, intro corresponds to Strategy 1.1.22, proving implications, and each impl_elim corresponds to Strategy 1.1.25, assuming implications.

Use implications backward: `apply`

The same argument can be driven entirely by the goal. If the goal is R and we have hqr : Q → R, then apply hqr changes the goal to Q: proving Q will be enough. Another apply reduces that goal to P.

example (hpq : P → Q) (hqr : Q → R) : P → R := by
  intro hp
  apply hqr
  apply hpq
  exact hp

The forward version with impl_elim asks, “What can I deduce from my assumptions?” The backward version with apply asks, “What would be enough to prove my goal?” They use the same logical rule in opposite working directions.

Disjunction: “or”

Proving P ∨ Q: prove either one of the two alternatives.

Assuming P ∨ Q: argue by cases, reaching the same goal from each alternative.

Introduce a disjunction: choose a side

A conjunction requires proofs of both parts, but a disjunction requires a proof of only one part. If we have hp : P, then disj_intro_left hpq from hp Q builds and names a proof hpq : P ∨ Q. The final Q tells Lean what the other proposition is.

example (hp : P) : P ∨ Q := by
  disj_intro_left hpq from hp Q
  exact hpq

If instead we have hq : Q, we introduce the right side. Here the extra P tells Lean what proposition belongs on the left.

example (hq : Q) : P ∨ Q := by
  disj_intro_right hpq from P hq
  exact hpq

These are the two disjunction introduction rules. In the textbook, they lead to Strategy 1.1.13: to prove P ∨ Q, it suffices to prove one of P or Q. Which side you choose matters—you should choose a side that your assumptions allow you to prove.

Eliminate a disjunction: proof by cases

Something new happens when eliminating a disjunction. If we know P ∨ Q, then we only know that at least one of P or Q is true, but we don't know which one. The only way we can prove a statement R in this situation is if we can prove it both from P and from Q. This means that the elimination rule for disjunctions produces two goals:

In the first case, Lean gives us hp : P.
In the second case, Lean gives us hq : Q.

We must prove the original goal in both cases. For example, disjunction is commutative:

example (h : P ∨ Q) : Q ∨ P := by
  disj_elim hp hq from h
  disj_intro_right hqp from Q hp
  exact hqp
  disj_intro_left hqp from hq P
  exact hqp

In the P case, we prove Q ∨ P using its right side. In the Q case, we prove the same goal using its left side. This is disjunction elimination, the proof-by-cases method described in Strategy 1.1.16. A case split succeeds only when every case reaches the same goal.

Use Lean's `cases` tactic

The tactic cases h also eliminates h : P ∨ Q. Lean names the two possible ways a proof of a disjunction can have been constructed: inl for a proof coming from the left and inr for a proof coming from the right. The corresponding case blocks focus on one goal at a time and give names to the new assumptions.

example (h : P ∨ Q) : Q ∨ P := by
  cases h
  case inl hp =>
    apply Or.intro_right
    exact hp
  case inr hq =>
    apply Or.intro_left
    exact hq

In case inl hp, Lean gives us hp : P; in case inr hq, it gives us hq : Q. Both branches must prove the original goal Q ∨ P. The names Or.intro_right and Or.intro_left are longer forms of Or.inr and Or.inl.

While constructing either branch in the web editor, keep sorry as its final line until the branch is finished. This prevents an incomplete branch from being reported only under All Messages and gives you a place where the current goal remains visible.

Let the goal lead with `apply`

As with conjunction and implication, we can work backward from a disjunction goal. If the goal is Q ∨ P, then apply Or.inr chooses the right alternative and changes the goal to P. Similarly, apply Or.inl chooses the left alternative and changes the goal to Q.

example (h : P ∨ Q) : Q ∨ P := by
  disj_elim hp hq from h
  apply Or.inr
  exact hp
  apply Or.inl
  exact hq

The two proofs of commutativity make the same logical moves. The first builds and names each new disjunction before using exact; the second simplifies each goal directly with apply.

Disjunctions can be nested

Lean reads P ∨ Q ∨ R as P ∨ (Q ∨ R). In the next example, eliminating hpq : P ∨ Q produces two cases. If P is true, introduce the left side of the goal. If Q is true, the assumption hqr : Q ∨ R already proves the entire right side, so introduce that side.

example (hpq : P ∨ Q) (hqr : Q ∨ R) : P ∨ Q ∨ R := by
  disj_elim hp hq from hpq
  disj_intro_left h from hp (Q ∨ R)
  exact h
  disj_intro_right h from P hqr
  exact h

The parenthesized argument (Q ∨ R) tells disj_intro_left the complete proposition on the right. This is another reason to keep track of how the operators are grouped.

A case that leads to contradiction

Lean treats ¬ P as P → False. Suppose we know ¬ P ∨ Q and want to prove P → Q. After assuming P, eliminate the disjunction:

In the ¬ P case, implication elimination combines P and ¬ P to produce False. The tactic exfalso changes the current goal from Q to False, which we can prove with that contradiction.
In the Q case, the assumption hq : Q is already exactly the goal.

example (h : ¬ P ∨ Q) : P → Q := by
  intro hp
  disj_elim hnp hq from h
  impl_elim f from hp hnp
  exfalso
  exact f
  exact hq

This proof combines implication introduction, disjunction elimination, implication elimination, and the principle that a contradiction implies any proposition. It also illustrates why both branches of a case split must be completed even when they finish in different ways.

Negation and contradiction

Proving ¬ P: assume P and prove False.

Assuming ¬ P: combine it with a proof of P to obtain False.

Reveal the implication with `change`

In Lean, ¬ P is notation for P → False. The change tactic replaces a goal or assumption by an equal expression that makes its useful logical structure visible. It does not change what must be proved.

example : ¬ (P ∧ ¬ P) := by
  change P ∧ ¬ P → False
  intro h
  conj_elim hp hnp from h
  change P → False at hnp
  apply hnp
  exact hp

The first change exposes the implication hidden in the goal. After intro h and conjunction elimination, the second change exposes the implication hidden in hnp : ¬ P. Applying hnp changes the goal from False to P, which is exactly the assumption hp.

The same idea proves the contrapositive form used in Lecture 5:

example (h : P → Q) (hnq : ¬ Q) : ¬ P := by
  change P → False
  intro hp
  change Q → False at hnq
  apply hnq
  apply h
  exact hp

Eliminate `False`

A proof of False has no possible cases. Therefore, if h : False, the command cases h closes any goal without producing a new branch. This is the principle that a contradiction implies anything.

example : False → P := by
  intro h
  cases h

If the current goal is some proposition Q and you intend to derive a contradiction, exfalso changes the goal to False. This is the goal-oriented form of the same principle.

Classical reasoning and excluded middle

Lean's core logic does not assume that every proposition is either true or false. After open Classical, the theorem em P supplies a proof of the law of excluded middle, P ∨ ¬ P.

open Classical

example : P ∨ ¬ P := by
  exact em P

Because em P is a disjunction, we can use cases em P to divide a classical proof into the case where P holds and the case where ¬ P holds.

example (h : P → Q) : ¬ P ∨ Q := by
  cases em P
  case inl hp =>
    apply Or.intro_right
    apply h
    exact hp
  case inr hnp =>
    apply Or.intro_left
    exact hnp

Mixing the operators

Real proofs alternate between introduction and elimination. To prove P → Q → R, introduce its two implications. Then build the conjunction required by the assumed implication P ∧ Q → R, use that implication, and finish with the result.

example (h : P ∧ Q → R) : P → Q → R := by
  intro hp
  intro hq
  conj_intro hpq from hp hq
  impl_elim hr from hpq h
  exact hr