Annotations can be associated with a lemma declaration using square brackets after the lemma name, for example, lemma example [use_induction]. Adding annotations can change how a lemma is proven, e.g., by using induction as in the example just given. Annotations can also specify that a lemma is an auxiliary lemma, intended to be reused in the proof of other lemmas. Moreover, as we have seen in Chap. 8, a sources annotated lemma is proven using induction and the sources lemma additionally changes the sources used for all other proofs. In this chapter, we explain the use of the lemma annotations use_induction, reuse, and hide_lemma. There is a further lemma annotation heuristic to specify lemma-specific heuristics, which we will return to in Sect. 16.4. In equivalence mode, lemmas can also be annotated with left, right, or both, as explained in Sect. 13.1.