## Stream: new members

### Topic: How to write this in proof in tactic style

#### Luis Berlioz (Aug 15 2019 at 20:10):

Hi, I am trying to write the following proof completely in tactic mode. I don't know how to use tactics with the second by_contradiction statement. Even though the proof works as it written now, currently I am learning about tactic mode so I want to know how to do it even if it is not practical. Thanks.

open classical
example : (¬∀ x, p x)  ( x, ¬p x) :=
begin
intros hnA,
intro hnE,
have :  (x : α), p x, from
assume s: α,
(assume hs: ¬p s,
show false, from hnE  s, hs ),
show false, from absurd this hnA,
end

#### Yury G. Kudryashov (Aug 15 2019 at 20:23):

Copy+pasted your example, defined {α : Type*} {p : α → Prop}. It doesn't work. Do you have any imports?

#### Rob Lewis (Aug 15 2019 at 20:24):

He has the classical namespace open.

#### Rob Lewis (Aug 15 2019 at 20:24):

One way to do it is this, which uses the by_contradiction tactic:

example : (¬∀ x, p x)  ( x, ¬p x) :=
begin
intro hnA,
have :  (x : α), p x,
{ intro s,
show false, from hne s, hs },
show false, from absurd this hnA,
end

#### Luis Berlioz (Aug 15 2019 at 20:28):

added the import. Thanks!

#### Yury G. Kudryashov (Aug 15 2019 at 20:28):

section
local attribute [instance] classical.prop_decidable

example {α : Type} {p : α  Prop} : (¬∀ x, p x)  ( x, ¬p x) :=
begin
intros hnA,
apply hnA,
intro x,
apply hne,
exact x, hx
end
end

#### Yury G. Kudryashov (Aug 15 2019 at 20:28):

Another way to achieve the same goal.

#### Luis Berlioz (Aug 15 2019 at 20:39):

Nice! Thanks.

Last updated: May 12 2021 at 05:19 UTC