Introduction and elimination cheat sheet

∧ And `\and`

Introduction

From P and Q, conclude P ∧ Q.

pq

p ∧ q

```
apply And.intro
...
```
What Lean needsThe goal P ∧ Q.

What Lean doesReplaces it with two goals, P and Q.
```
conj_intro hpq from hp hq
```
What Lean needshp : P and hq : Q in the context.

What Lean doesAdds hpq : P ∧ Q to the context.
```
have hpq : P ∧ Q := ⟨hp, hq⟩
```
What Lean needshp : P and hq : Q in the context.

What Lean doesAdds hpq : P ∧ Q to the context.

Elimination

From P ∧ Q, conclude P and conclude Q.

p ∧ q

p

p ∧ q

q

```
conj_elim hp hq from hpq
```
What Lean needshpq : P ∧ Q in the context.

What Lean doesAdds hp : P and hq : Q to the context.
```
have ⟨hp, hq⟩ := hpq
```
What Lean needshpq : P ∧ Q in the context.

What Lean doesAdds hp : P and hq : Q to the context.
```
apply And.elim _ hpq
intro hp hq
...
```
What Lean needshpq : P ∧ Q in the context.

What Lean doesAdds hp : P and hq : Q to the context while retaining the current goal.

∨ Or `\or`

Introduction

From P, conclude P ∨ Q; from Q, conclude P ∨ Q.

p

p ∨ q

q

p ∨ q

```
disj_intro_left hpq from hp Q
```
What Lean needshp : P in the context.

What Lean doesAdds hpq : P ∨ Q to the context.
```
disj_intro_right hpq from P hq
```
What Lean needshq : Q in the context.

What Lean doesAdds hpq : P ∨ Q to the context.
```
apply Or.intro_left
...
```
What Lean needsThe goal P ∨ Q.

What Lean doesReplaces it with the goal P.
```
apply Or.intro_right
...
```
What Lean needsThe goal P ∨ Q.

What Lean doesReplaces it with the goal Q.
```
apply Or.inl
...
```
What Lean needsThe goal P ∨ Q.

What Lean doesReplaces it with the goal P.
```
apply Or.inr
...
```
What Lean needsThe goal P ∨ Q.

What Lean doesReplaces it with the goal Q.

Elimination

From P ∨ Q, derive the same conclusion from P and from Q.

p ∨ q [p] ⇝ r [q] ⇝ r

r

```
disj_elim hp hq from hpq
...
```
What Lean needshpq : P ∨ Q in the context.

What Lean doesCreates two copies of the current goal: one with hp : P in the context and one with hq : Q.
```
cases hpq
case inl hp => ...
case inr hq => ...
```
What Lean needshpq : P ∨ Q in the context.

What Lean doesCreates a case with hp : P and a case with hq : Q; both retain the current goal.
```
apply Or.elim hpq
· intro hp
  ...
· intro hq
  ...
```
What Lean needshpq : P ∨ Q in the context.

What Lean doesCreates two copies of the current goal: one under hp : P and one under hq : Q.

→ Implies `\to`

Introduction

To prove P → Q, assume P and derive Q.

[p] ⇝ q

p ⇒ q

```
intro hp
...
```
What Lean needsThe goal P → Q.

What Lean doesAdds hp : P to the context and replaces the goal with Q.

Elimination

From P → Q and P, conclude Q.

p ⇒ qp

q

```
impl_elim hq from hp hpq
```
What Lean needshpq : P → Q and hp : P in the context.

What Lean doesAdds hq : Q to the context.
```
have hq := hpq hp
```
What Lean needshpq : P → Q and hp : P in the context.

What Lean doesAdds hq : Q to the context.
```
apply hpq
...
```
What Lean needshpq : P → Q in the context and the goal Q.

What Lean doesReplaces the goal with P.

¬ Not `\neg`

Introduction

To prove ¬P, assume P and derive a contradiction.

[p] ⇝ ⊥

¬p

```
change P → False
```
What Lean needsThe goal ¬ P.

What Lean doesRewrites the goal as P → False.
```
change ¬ P at h
```
What Lean needsh : P → False in the context.

What Lean doesRewrites the hypothesis as h : ¬ P.

Elimination

From ¬P and P, derive a contradiction.

¬pp

⊥

```
contradiction
```
What Lean needsContradictory hypotheses, such as hp : P and hnp : ¬ P, in the context.

What Lean doesCloses the current goal.

↔ If and only if `\iff`

Introduction

Prove P → Q and prove Q → P.

p ⇒ qq ⇒ p

p ⇔ q

```
apply Iff.intro
```
What Lean needsThe goal P ↔ Q.

What Lean doesReplaces it with the goals P → Q and Q → P.

Elimination

Use either implication: P → Q or Q → P.

p ⇔ q

p ⇒ q

p ⇔ q

q ⇒ p

```
apply Iff.elim _ h
intro hpq hqp
...
```
What Lean needsh : P ↔ Q in the context.

What Lean doesAdds hpq : P → Q and hqp : Q → P to the context while retaining the current goal.

∀ For every `\forall`

Introduction

For arbitrary t : T, derive P t.

[x ∈ X] ⇝ p(x)

∀x ∈ X, p(x)

```
intro t
...
```
What Lean needsThe goal ∀ x : T, P x.

What Lean doesAdds an arbitrary t : T to the context and replaces the goal with P t.

Elimination

From ∀ x : T, P x, conclude P t for t : T.

∀x ∈ X, p(x)a ∈ X

p(a)

```
have := h t
...
```
What Lean needsh : ∀ x : T, P x and t : T in the context.

What Lean doesAdds this : P t to the context.
```
have hpt := h t
...
```
What Lean needsh : ∀ x : T, P x and t : T in the context.

What Lean doesAdds hpt : P t to the context.

∃ There exists `\exists`

Introduction

Choose t : T and prove P t.

a ∈ Xp(a)

∃x ∈ X, p(x)

```
apply Exists.intro t
...
```
What Lean needsThe goal ∃ x : T, P x and an available term t : T.

What Lean doesChooses t as the witness and replaces the goal with P t.

Elimination

From ∃ x : T, P x, introduce a new t : T and assume P t.

∃x ∈ X, p(x) [a ∈ X], [p(a)] ⇝ q

q

```
obtain ⟨t, hpt⟩ := h
...
```
What Lean needsh : ∃ x : T, P x in the context.

What Lean doesAdds a new witness t : T and hpt : P t to the context.
```
apply Exists.elim h
intro t
intro hpt
...
```
What Lean needsh : ∃ x : T, P x in the context.

What Lean doesAdds a new t : T and hpt : P t to the context while retaining the current goal.

∧ And \and

Introduction

Elimination

∨ Or \or

Introduction

Elimination

→ Implies \to

Introduction

Elimination

¬ Not \neg

Introduction

Elimination

↔ If and only if \iff

Introduction

Elimination

∀ For every \forall

Introduction

Elimination

∃ There exists \exists

Introduction

Elimination

∧ And `\and`

∨ Or `\or`

→ Implies `\to`

¬ Not `\neg`

↔ If and only if `\iff`

∀ For every `\forall`

∃ There exists `\exists`