# 2.11 Existential Quantifiers

An existential statement says that some object exists with a given property. In Lean, a proof of `Exists P` contains two pieces of data: a witness and a proof that the witness satisfies the predicate.

The usual mathematical notation:

```lean
∃ x, P x
```

means:

```lean
Exists (fun x => P x)
```

## Problem

You want to prove or use a statement of the form:

```lean
∃ x : α, P x
```

To prove it, provide a witness `x` and then prove `P x`. To use it, unpack the witness and its proof.

## Solution

Use `use` to provide a witness.

```lean
theorem exists_nat_example : ∃ n : Nat, n = 3 := by
  use 3
```

After `use 3`, the goal becomes:

```lean
⊢ 3 = 3
```

Lean closes it by reflexivity.

A more explicit version is:

```lean
theorem exists_nat_example_explicit : ∃ n : Nat, n = 3 := by
  use 3
  rfl
```

## Providing a Witness with a Nontrivial Proof

The witness fixes the remaining goal.

```lean
theorem exists_even_example : ∃ n : Nat, n + n = 6 := by
  use 3
```

After `use 3`, Lean checks:

```lean
⊢ 3 + 3 = 6
```

This reduces by computation.

For a proof that needs a library theorem:

```lean
theorem exists_add_zero (a : Nat) : ∃ n : Nat, a + n = a := by
  use 0
  simp
```

The witness is `0`. The remaining goal is:

```lean
⊢ a + 0 = a
```

which `simp` proves.

## Constructing Existentials Directly

The constructor for existential statements is `Exists.intro`.

```lean
theorem exists_intro_term : ∃ n : Nat, n = 3 :=
  Exists.intro 3 rfl
```

The first argument is the witness. The second argument is the proof that the witness satisfies the predicate.

For:

```lean
∃ n : Nat, n = 3
```

the witness is:

```lean
3
```

and the proof is:

```lean
rfl : 3 = 3
```

## Using an Existential Hypothesis

If you have:

```lean
h : ∃ x : α, P x
```

then you can extract a witness and its property proof by case analysis.

```lean
theorem exists_use_example
    (h : ∃ n : Nat, n = 3) :
    ∃ m : Nat, m + 1 = 4 := by
  cases h with
  | intro n hn =>
    use n
    rw [hn]
```

After `cases h`, Lean gives:

```lean
n : Nat
hn : n = 3
⊢ ∃ m : Nat, m + 1 = 4
```

The proof uses the same witness `n`, then rewrites `n` to `3`.

## Destructuring with `rcases`

For existential hypotheses, `rcases` gives compact destructuring.

```lean
theorem exists_use_rcases
    (h : ∃ n : Nat, n = 3) :
    ∃ m : Nat, m + 1 = 4 := by
  rcases h with ⟨n, hn⟩
  use n
  rw [hn]
```

The pattern:

```lean
⟨n, hn⟩
```

extracts the witness `n` and the proof `hn`.

## Existentials with Multiple Conditions

Existential predicates often contain conjunctions.

```lean
theorem exists_with_and : ∃ n : Nat, n = 3 ∧ n + 1 = 4 := by
  use 3
  constructor
  · rfl
  · rfl
```

After `use 3`, the goal is:

```lean
⊢ 3 = 3 ∧ 3 + 1 = 4
```

Then `constructor` splits the conjunction.

## Using Existentials with Conjunctions

When an existential contains a conjunction, unpack both layers.

```lean
theorem exists_and_use
    (h : ∃ n : Nat, n = 3 ∧ n + 1 = 4) :
    ∃ n : Nat, n + 1 = 4 := by
  rcases h with ⟨n, hn_eq, hn_add⟩
  use n
  exact hn_add
```

The pattern:

```lean
⟨n, hn_eq, hn_add⟩
```

is shorthand for unpacking:

```lean
⟨n, ⟨hn_eq, hn_add⟩⟩
```

The first component is the witness. The remaining components are proofs from the conjunction.

## Changing the Witness

Sometimes the output witness differs from the input witness.

```lean
theorem exists_successor
    (h : ∃ n : Nat, n = 3) :
    ∃ m : Nat, m = 4 := by
  rcases h with ⟨n, hn⟩
  use n + 1
  rw [hn]
```

After rewriting `n` to `3`, the goal becomes:

```lean
⊢ 3 + 1 = 4
```

which is solved by computation.

## Existentials Over Arbitrary Types

Existentials are not limited to natural numbers.

```lean
theorem exists_self
    (α : Type)
    (a : α) :
    ∃ x : α, x = a := by
  use a
```

The witness is the given value `a`.

A predicate version:

```lean
theorem exists_from_predicate
    (α : Type)
    (P : α -> Prop)
    (a : α)
    (ha : P a) :
    ∃ x : α, P x := by
  use a
```

After `use a`, the goal is exactly `P a`, which is already available as `ha`. Lean can close it, but an explicit version is clearer:

```lean
theorem exists_from_predicate_explicit
    (α : Type)
    (P : α -> Prop)
    (a : α)
    (ha : P a) :
    ∃ x : α, P x := by
  use a
  exact ha
```

## Existentials and Equality Transport

A common pattern is to unpack an existential, rewrite with an equality, and rebuild another existential.

```lean
theorem exists_transport
    (P : Nat -> Prop)
    (h : ∃ n : Nat, n = 3 ∧ P n) :
    P 3 := by
  rcases h with ⟨n, hn_eq, hnP⟩
  rw [← hn_eq]
  exact hnP
```

Here `hn_eq : n = 3`. The goal is `P 3`, while the available proof is `hnP : P n`. Rewriting backward changes `P 3` to `P n`.

## Nested Existentials

Multiple existential quantifiers are nested.

```lean
theorem exists_pair_example :
    ∃ n : Nat, ∃ m : Nat, n = m := by
  use 3
  use 3
```

This means:

```lean
∃ n : Nat, (∃ m : Nat, n = m)
```

To unpack:

```lean
theorem exists_pair_use
    (h : ∃ n : Nat, ∃ m : Nat, n = m) :
    ∃ k : Nat, k = k := by
  rcases h with ⟨n, m, hnm⟩
  use n
```

The pattern `⟨n, m, hnm⟩` unpacks both existential layers.

## Existentials and `apply`

You can construct an existential with `apply Exists.intro`.

```lean
theorem exists_apply_intro : ∃ n : Nat, n = 5 := by
  apply Exists.intro 5
  rfl
```

This is more verbose than `use`, but it exposes the constructor.

## Common Patterns

To prove:

```lean
⊢ ∃ x : α, P x
```

use:

```lean
use a
```

then prove:

```lean
⊢ P a
```

To use:

```lean
h : ∃ x : α, P x
```

use:

```lean
rcases h with ⟨x, hx⟩
```

or:

```lean
cases h with
| intro x hx => ...
```

To prove an existential with several properties:

```lean
use a
constructor
```

To unpack nested existential and conjunction data:

```lean
rcases h with ⟨x, hx₁, hx₂⟩
```

## Common Pitfalls

Do not try to prove an existential without choosing a witness. Lean needs a concrete term for the quantified variable.

Do not assume the witness has a particular name. After unpacking an existential, choose names that reflect how the witness will be used.

Do not forget that `∃ x, P x ∧ Q x` contains a witness and then a conjunction of proofs. You must unpack both layers when needed.

Do not rewrite in the wrong direction when moving a property from the witness to a known value.

## Takeaway

An existential proof is a witness plus evidence. To prove `∃ x, P x`, provide a witness and prove the predicate for that witness. To use `∃ x, P x`, unpack the witness and the proof, then continue with those concrete objects in the local context.