Checking Predicate Logic Using Coq - Beginner Syntax

Question

I am trying to prove the following in Coq:

Target (forall x: X, P (x) / \ Q (x)) → ((for all x: X, P (x)) / \ (for all x: X, Q (x))).

Can anybody help? I am not sure to split, make an assumption, etc.

I apologize for being a complete noob

Answer 1

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.

Answer 2

Just a few tips: I recommend you use an intro to name your hypothesis, split it to separate goals, and accurate to provide evidence (which may include proj1 or proj2).