ゴールが前提や既にある定理そのものである場合が、証明の一番簡単なパターンです。

前提がゴールそのものである場合

assumptionを使うと、前提にあるゴールと全く同じ命題をそのまま適用してくれます。

Goal forall P : Prop, P -> P.
Proof.
  intros. (* P : Prop, H : P *)
  assumption.
Qed.

外部の定理がゴールそのものである場合

前提や定理Tに対してapply Tを使うと、ゴールにTを適用できます。

Theorem Sn_is_not_O: forall n : nat, S n <> O.
Proof.
  congruence.
Qed.

Goal forall n : nat, S n <> O. (* Sn_is_not_O と全く同じ *)
Proof.
  apply Sn_is_not_O.
Qed.

また、この場合はapplyではなくexactも使うことができます。

Goal forall n : nat, S n <> O.
Proof.
  exact Sn_is_not_O.
Qed.

前提や定理にP, P -> Qがあり、ゴールがQである場合

ゴールが「…ならば…」の結論部分である場合も、applyが使えます。

Goal forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
  intros P Q H1 H2. (* H1 : P, H2 : P -> Q *)
  (* Goal: Q *)
  apply H2 in H1. (* H1 : Q に変わる *)
  assumption.
Qed.

前提がforall x, P xの形であり、ゴールがP aである場合

この場合でもapplyが使えます。

Goal forall P : nat -> Prop,
       (forall n : nat, P n) -> P 5.
Proof.
  intros P H. (* H : forall n : nat, P n *)
  apply H.
Qed.