theorem-proving - LEAN の第一原理から (¬ ∀ x, px) → (∃ x, ¬ px) をどのように証明できますか?

Question

第一原理からのこの基本的な含意の証明、「リーンでの定理の証明」4.4 の演習は、これまでの私のすべての試みよりも優れています。

open classical
variables (α : Type) (p q : α → Prop)
variable a : α

local attribute [instance] classical.prop_decidable
theorem T08R : (¬ ∀ x, p x) → (∃ x, ¬ p x) := 
begin
    intro nAxpx, 
    --by_contradiction nExnpx,
    --apply nAxpx,
end

その後、さらに先に進むintro方法がわかりません。nAxpxと思ったのですが、それは では使えないby_contradiction否定的な存在を紹介するだけなので、 は出せません。除外された中間も役に立たないようです。戦術で証明できるし、nExnpxcasesx : αmathlib

theorem T08R : (¬ ∀ x, p x) → (∃ x, ¬ p x) := 
begin
    push_neg,
    tauto
end

しかし、それを戦術モードに変換するのに十分な知識がないため、これは私の理解には役立ちません.