Proving Predicate Logic using Coq - Beginner Syntax

Question

I'm trying to prove the following in Coq:

Goal (forall x:X, P(x) /\ Q(x)) -> ((forall x:X, P (x)) /\ (forall x:X, Q (x))).

Can someone please help? I'm not sure whether to split, make an assumption etc.

My apologies for being a complete noob

Answer 1

Just some hints: I recommand you use intros to name your hypothesis, split to separate the goals, and exact to provide the proof terms (which may involve proj1 or proj2).

Answer 2

Goal forall (X : Type) (P Q : X->Prop), 
    (forall x : X, P x /\ Q x) -> (forall x : X, P x) /\ (forall x : X, Q x).
Proof.
  intros X P Q H; split; intro x; apply (H x).
Qed.