One activity at this meeting will be to brainstorm tools (broadly construed) that will help with the formalization of analysis. Tools are not themselves formal proofs in Lean; often they take the form of *metaprograms*, pieces of code that interact with Lean expressions in various ways. (Tactics are the most familiar kind of metaprogram to most Lean users.) In this talk I will introduce the basic components of a Lean metaprogram and describe different tactic design strategies, including proof by reflection and proof by certificate. Better understanding of the basic building blocks of Lean tooling will help brainstorm new ideas and applications.