Another hard goal (for me, of course) is the following:
Goal ~(forall P Q: nat -> Prop,
(exists x, P x) /\ (exists x, Q x) ->
(exists x, P x /\ Q x)).
Proof.
I absolutely have no idea of what could I do. If I introduce something, I get a universal quantifier in the hypotesis, and then I can't do anything with it.
I suppose that it exists a standard way for managing such kind of situations, but I was not able to find it out.
To progress in that proof, you will have to exhibit an instance of P and an instance of Q such that your hypothesis produces a contradiction.
A simple way to go is to use:
P : fun x => x = 0
Q : fun x => x = 1
In order to work with the hypothesis introduced, you might want to use the tactic specialize:
Goal ~(forall P Q : nat -> Prop,
(exists x, P x) /\ (exists x, Q x) ->
(exists x, P x /\ Q x)).
Proof.
intro H.
specialize (H (fun x => x = 0) (fun x => x = 1)).
It allows you to apply one of your hypothesis on some input (when the hypothesis is a function). From now on, you should be able to derive a contradiction easily.
Alternatively to specialize, you can also do:
pose proof (H (fun x => x = 0) (fun x => x = 1)) as Happlied.
Which will conserve H and give you another term Happlied (you choose the name) for the application.