Feature request: SMT trigger annotations

[atomb]

When sending quantified assumptions through the SMT backend, quantifier instantiation can greatly affect performance (and even completeness). Boogie and Dafny are example tools that have made heavy use of trigger annotations to guide the solver (Z3, generally) to choose useful instantiations. I suspect it would be possible to add some sort of mechanism for writing annotations on quantified terms that don't have semantic significance within Lean but could be used to control trigger annotations in SMT-Lib formulas. (Other provers could probably just ignore them.)