# Zulip Chat Archive

## Stream: new members

### Topic: Exists

#### Thomas Brooks (Jul 04 2020 at 22:29):

Hi, I'm working through the documentation and exercises and I'm stuck on 4.4 (existential quantifier). I thought I could use exists.elim to go from `\exists (x: \alpha), p x`

to `x`

but I get a type error since `x`

is not a Prop. I seem to need this to prove the reverse direction of the exercise `example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r`

. Any guidance? My full attempt is:

```
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
iff.intro
(assume (h: ∃ x, p x ∧ r),
exists.elim h
(assume (hx: α) (hpxr: p hx ∧ r),
(and.intro
(exists.intro
hx
hpxr.left)
hpxr.right)))
(assume (h: (∃ x, p x) ∧ r),
exists.intro
(exists.elim h.left
(assume (hx: α) (hpx: p hx),
hx)) -- Problem here!! has type Π (hx : α), p hx → α : Type
(exists.elim h.left
(assume (hx: α) (hpx: p hx),
show p hx ∧ r, from and.intro hpx h.right)))
```

#### Reid Barton (Jul 04 2020 at 22:30):

You should use `exists.elim`

while your goal is still a Prop.

#### Kevin Buzzard (Jul 04 2020 at 22:31):

This is much easier in tactic mode

#### Thomas Brooks (Jul 04 2020 at 22:33):

I haven't gotten to tactics yet!

#### Thomas Brooks (Jul 04 2020 at 22:34):

@Reid Barton I'm not sure what you mean. Is `exists.elim`

not appropriate here? Is there an alternative?

#### Thomas Brooks (Jul 04 2020 at 22:36):

And on this topic, how can I view everything in a namespace? Like to look at all everything that is exists.something to see if something fits my needs.

#### Thomas Brooks (Jul 04 2020 at 22:36):

Oh wait, I think I understand now. I should use exist.elim outside of the exists.intro....

#### Thomas Brooks (Jul 04 2020 at 22:45):

That fixed it, thanks for the help. So is there no way to get `(\exists x: \alpha, p x) -> \alpha`

? I would have assumed that could be done

#### Kyle Miller (Jul 04 2020 at 23:02):

@Thomas Brooks It's sort of a coherence issue. You need to choose an term of `\alpha`

in a consistent way so that substitution/rewriting works. One thing to think about is that, since every pair of proofs of a `Prop`

are equal, you can't just take a proof `⟨x, h⟩`

of existence and map it to `x`

. What would you do for `⟨x', h'⟩`

? You'd need to ensure that whatever you did wouldn't give you the absurd conclusion that `x = x'`

.

The library has `classical.some`

to "give" you such a term (noncomputably). It uses Lean's version of the axiom of choice.

#### Thomas Brooks (Jul 04 2020 at 23:21):

@Kyle Miller That makes sense, thanks for the explanation!

#### Kevin Buzzard (Jul 04 2020 at 23:45):

`#print prefix exists`

#### Jason Orendorff (Jul 04 2020 at 23:45):

`#print prefix`

is so darn useful, it should be mentioned earlier in the book

Last updated: May 08 2021 at 03:17 UTC