Как можно доказать (¬ ∀ x, px) → (∃ x, ¬ px) из первых принципов LEAN?

Question

Доказательство этого базового c следствия из первых принципов, упражнение из "Доказательство теоремы в Lean" 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 до go дальше. Я думал о by_contradiction, но это только вводит отрицательное существование nExnpx, которое нельзя использовать с cases, поэтому я не могу создать x : α. Исключенная середина, кажется, также не помогает. Я могу получить доказательство с помощью mathlib тактики,

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

, но у меня недостаточно знаний, чтобы перевести это обратно в режим тактики, так что это не поможет моему пониманию.

Answer 1

Я думаю, вам нужно сделать by_contradiction дважды. После apply naXpx попробуйте intro a, а затем by_contradiction. Тогда у вас будет a доказательство ¬p a, а также доказательство того, что ¬∃ (x : α), ¬p x, что является противоречием.

Полное доказательство

theorem T08R : (¬ ∀ x, p x) → (∃ x, ¬ p x) := 
begin
    intro nAxpx, 
    by_contradiction nExnpx,
    apply nAxpx,
    assume a,
    by_contradiction hnpa,
    apply nExnpx,
    existsi a,
    exact hnpa,
end