(∃y ∈ A, P y) ∨ (∃y ∈ A, Qy) =⇒ ∃x ∈ A, P x ∨ Qx is a school hw problem of mine, and I haven't encountered something of this nature yet and I' not sure where to start really. So if anyone is good at teaching this stuff or knows a great resource to familiarize myself with this that would be great. If you just want to show it in the proof assistant that is also helpful, but i would really like how to understand how to do these.
I'm sorry if the way this is worded breaks tos ahead of time, I'm rather new to these stack sites, A friend of mine told me about them but said to be careful.