How to write this in proof in tactic style

Stream: new members

[Luis Berlioz]

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,
  apply by_contradiction,
   intro hnE,
  have : ∀ (x : α), p x, from
     assume s: α,
    by_contradiction
        (assume hs: ¬p s,
        show false, from hnE ⟨ s, hs ⟩),
    show false, from absurd this hnA,
end

[Yury G. Kudryashov]

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

[Rob Lewis]

He has the classical namespace open.

[Rob Lewis]

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

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

[Luis Berlioz]

added the import. Thanks!

[Yury G. Kudryashov]

section
local attribute [instance] classical.prop_decidable

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

[Yury G. Kudryashov]

Another way to achieve the same goal.

[Luis Berlioz]

Nice! Thanks.