  This paper introduces norm_cast, a toolbox of tactics for the Lean proof
assistant designed to manipulate expressions containing coercions and casts.
These expressions can be frustrating for beginning and expert users alike; the
presence of coercions can cause seemingly identical expressions to fail to
unify and rewrites to fail. The norm_cast tactics aim to make reasoning with
such expressions as transparent as possible. They are used extensively to
eliminate boilerplate arguments in the Lean mathematical library and in
external developments.
