I have been limping along in Dafny without understanding triggers. Perhaps as a result, the programs I write seem to give the verifier a hard time. Sometimes I spend tons of time fiddling with my proof, trying to convince Dafny/Boogie that it's valid; and when I get something working, sometimes it's slow to verify (which seriously degrades my ability to continue).
It's hard to ask a precise question, because I don't know what it is I don't know. But let's start with the basics:
What are triggers? When are they used? How are they inferred? And once I understand all that, what should I read next?
Understanding triggers is definitely an important part of becoming an expert at Dafny!
We have recently started a frequently asked questions page for Dafny, which includes a fairly extensive description of triggers. I recommend you start by reading that part of the FAQ. (The rest of this answer assumes you have done so.)
One thing that's not covered there is how triggers are inferred. (I will add an edited version of this answer to the FAQ soon.) Triggers are actually potentially inferred at two different levels: by Dafny or by Z3. Generally, it is better if the trigger is inferred at the Dafny level, because is more likely to find a concise trigger before all the encoding details from translating to Z3 get involved. However, if Dafny does not manage to infer a trigger, sometimes Z3 can still do something useful as a stopgap. (In such cases, Dafny issues a warning.)
The inference procedure used by both Z3 and Dafny are conceptually quite similar. Given a quantified expression forall x1, ..., xn :: e, the inference procedure tries to find subexpressions of e that involve only variables, constants, and uninterpreted functions/predicates such that each xi appears in the subexpression. For example, in the expression
forall a, b :: P(a) && Q(a, b) ==> R(b)
the expression Q(a, b) is a valid trigger, since it mentions all the bound variables and doesn't include any interpreted functions. Another valid trigger is the set of expression {P(a), R(b)}. Whether one trigger or the other (or both) is better depends on the context. Typically Dafny will infer and use all valid, maximally general triggers, so in this case it would select both Q(a, b) and {P(a), R(b)}.
In general, Dafny's trigger inference works by enumerating all valid triggers by looking at all subexpressions of e. Dafny then filters out triggers that are strictly less general than another valid trigger. Dafny selects all remaining triggers.
For additional reading, I recommend the paper Simplify: A Theorem Prover for Program Checking by Detlefs, Nelson, and Saxe. Simplify was an early SMT solver that pioneered the heuristic use of triggers to handle quantifiers. Section 5 of the paper above describes the approach in technical detail.