universal quantification elimination

Stream: lean4

[Yasu Watanabe]

I'm learning lean4 with Theorem Proving in Lean 4 and I'm stuck in proving

example : (∀ x, p x ∨ r) → (∀ x, p x) ∨ r := sorry

I think to prove this, taking arbitrary a into hypothesis is needed but I don't know how to express this. I'd like to prove this with tactic since it provides me proof object too.

[Mario Carneiro]

Hint: use by_cases hr : r to consider the cases where r is true or false. In either case the problem simplifies to something you can prove

[Mario Carneiro]

Hint 2: you don't need a (you will for a later exercise though)

[Yasu Watanabe]

Ah, I see. I completely missed the text below.

Try proving these (one direction of the second of these requires classical logic):
I'll try it based on your hints. Thanks.