Another new member question

Stream: lean4

[kvanvels]

Hi, Please let me know if there is a better place for these question. I don't want to be a pest. I posted this question as follow-up to a question I asked yesterday, feel free to delete either question.

I am trying to prove the following exercise (trimmed down version) of an exercise in "Theorem proving in Lean". I have posted my best approach.

open Classical

variable (α : Type) (p q : α → Prop)
variable (r : Prop)

example (a : α) :  ((∀ x, p x) → r)  → (∃ x, p x → r) :=
(fun h : (∀ x, p x) → r =>
  suffices h2 : p a → r from Exists.intro a h2
  fun h3 : p a =>
  suffices h4 : (∀ (x : α), p x) from (h h4)
  fun x => _ --don't know what I should do here.
 )

I need to show (p x) and have (p a) for every a in α. So this should be sufficient. How do I tell lean4 to notice this? Any help will be appreciated.

There is some discussion about this in the tutorial, (there is a paragraph that reads : As was the case for implication, the propositions-as-types interpretation now comes into play. Remember the introduction and elimination rules for dependent arrow types: and then an example but I can't see how to use it)

[Kevin Buzzard]

@kvanvels just to clarify: you are welcome to ask beginner Lean 4 questions in this stream; indeed it's exactly the right place to ask them.

[Kevin Buzzard]

As to your question, your goal does not look provable to me; maybe you took a wrong turn? I don't understand your claim "I have p a for every a in α"; in your goal state a is a fixed element of α.

[Ruben Van de Velde]

Are you sure the statement has its parentheses in the right place?

[Kevin Buzzard]

Oh I think this (with the brackets as they are) isn't true constructively; you'll have to split on whether r is true or false, I don't think you can just follow your nose like you're doing.

[Ruben Van de Velde]

Ah, that works indeed, or on (∀ x, p x) being true or false

[kvanvels]

I found the answer to this exercise in the book. It is quite a bit more complicated than I expected. I appreciate the responses.