# Zulip Chat Archive

## Stream: new members

### Topic: exists_elim

#### Michael Beeson (Jun 20 2020 at 16:54):

Below I will paste in a correct proof. My question is, please show me a couple of better ways to prove this simple theorem.

Q1: how can I do this without entering tactic mode? Q2: how can I do it entirely in tactic mode, i.e., what do I use in tactic mode that corresponds to exists.elim?

```
variables (p q r : nat→ Prop)
lemma test3 :
(∃ x:nat ,( p x ∧ q x ∧ r x) )→ (∃x:nat, (r x) ):=
assume h,
exists.elim h
begin
intros a h2,
existsi a,
exact h2.right.right,
end
```

#### Bryan Gin-ge Chen (Jun 20 2020 at 16:59):

```
variables (p q r : nat→ Prop)
-- Q1
lemma test3_term :
(∃ x:nat ,( p x ∧ q x ∧ r x) )→ (∃x:nat, (r x) ):=
assume h,
exists.elim h (assume a h2, exists.intro a h2.2.2)
-- Q2
lemma test3_tactic :
(∃ x:nat ,( p x ∧ q x ∧ r x) )→ (∃x:nat, (r x) ):=
begin
intro h,
cases h with a h2,
existsi a,
exact h2.2.2
end
```

#### Michael Beeson (Jun 20 2020 at 17:01):

Thank you. If there is a way to mark an answer as "the answer" like on stack exchange, I don't know it.

#### Bryan Gin-ge Chen (Jun 20 2020 at 17:03):

The proof using mathlib tactics is much nicer:

```
import tactic
lemma test3_tactic2 :
(∃ x:nat ,( p x ∧ q x ∧ r x) )→ (∃x:nat, (r x) ):=
begin
rintro ⟨a, h1, h2, h3⟩,
use [a, h3]
end
```

#### Bryan Gin-ge Chen (Jun 20 2020 at 17:05):

Or even shorter:

```
import tactic
lemma test3_tactic3 :
(∃ x:nat ,( p x ∧ q x ∧ r x) )→ (∃x:nat, (r x) ):=
by tauto
```

#### Jalex Stark (Jun 20 2020 at 17:37):

Michael Beeson said:

Thank you. If there is a way to mark an answer as "the answer" like on stack exchange, I don't know it.

you can react with emoji

#### Michael Beeson (Jun 20 2020 at 19:19):

'tauto' appears to be misnamed if it deals with quantifiers.

I am trying to work with intuitionistic logic only. Are there analogues for these tactics that are intuitionistic?

I notice that 'ifinish' can't handle this example. In general, once I have a proof, how can I ask Lean to check if

it is really an intuitionistic proof? I'm worried that some tactics may, in the words of Avigad in a comment in finish.lean,

"leak classical logic".

#### Johan Commelin (Jun 20 2020 at 19:19):

`#print axioms your_lemma_name`

#### Johan Commelin (Jun 20 2020 at 19:20):

If you see `classical.choice`

, something went wrong

Last updated: May 06 2021 at 21:09 UTC