- Comments are required when a Lean tactic is opaque in its meaning. - Lean `coding phrases` that are self-explanatory are mandated, such as using: - exact show *Goal* from *Hypothesis* instead of exact *Hypotheses*. - A set of macros is used to streamline the uniform application of these comments. Tactics whose name does not clearly identify its meaning require clarifying comments.