I am looking at this:
Theorem eq_add_1 : forall n m,
n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
Proof.
intros n m. rewrite one_succ. intro H.
assert (H1 : exists p, n + m == S p) by now exists 0.
apply eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H.
apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
Qed.
How do I find what the thing like intros or destruct mean exactly, like looking up an implementation (or if not possible, a definition)? What is the way to do this efficiently?
The answer differs for primitive and user-defined tactics. However, the proof script you show uses almost no user-defined tactics, except now, which is a notation for the easy tactic.
If you're not sure if a tactic is primitive, try both; checking the manual might be the simplest first step.
For tactics defined as Ltac foo args := body. you can use Print Ltac foo (e.g. Print Ltac easy.). AFAIK, that does not work for tactics defined by Tactic Notation. In both cases, I prefer to look at the sources (which I find via grep).
There is the Coq reference manual (https://coq.inria.fr/distrib/current/refman/coq-tacindex.html), which does not have complete specification but is usually the closest approximation. It’s not very accessible, so you should first refer to one of the many Coq tutorials or introductions, like Software Foundations.
There is the actual Coq implementation, but that’s not very helpful unless you’re a Coq implementer.