Between 2014 and 2016, I was using Coq regularly, but did not know that its Search command accepts patterns. If only I had learnt this earlier, this would have saved me so much time!

For instance, if I want to simplify a multiplication out of a modulo, I can find the right lemma using

Search ((_ * ?x) mod ?x).

which will return exactly the right lemmas:

Z_mod_mult: forall a b : Z, (a * b) mod b = 0
Z.mod_mul: forall a b : Z, b <> 0 -> (a * b) mod b = 0
Two caveats: I have to Require the modules containing these lemmas before, so in order to make the above work, I had to Require Import Coq.ZArith.ZArith. And I have to make sure the notations are interpreted in the right scope, either by Open Scope Z_scope., or by specifying the scope delimiter like ((_ * ?x) mod ?x)%Z.
Moreover, Search also accepts multiple patterns. For instance, to find all lemmas involving list equalities mentioning skipn, I can do

Search skipn (@eq (list _) _).

which will return

firstn_skipn: forall (A : Type) (n : nat) (l : list A), firstn n l ++ skipn n l = l
There's much more information for Search in the reference manual.
I'm collecting a list of more Coq tricks here, and later I learned that other people collect their tricks as well. For instance, Tej Chajed's list is here. If you have a collection of Coq tricks as well, please let me know!