mathlib3

5fd4afc4 - refactor(tactic/norm_cast): simplified attributes and numeral support (#2407)

refactor(tactic/norm_cast): simplified attributes and numeral support (#2407) This is @pnmadelaine's work, I'm just updating it to work with current mathlib. New and improved version of `norm_cast` as described in the paper "normalizing casts and coercions": https://arxiv.org/abs/2001.10594 The main new user-facing feature are the simplified attributes. There is now only the `@[norm_cast]` attribute which subsumes the previous `norm_cast`, `elim_cast`, `squash_cast`, and `move_cast` attributes. There is a new `set_option trace.norm_cast true` option to enable debugging output. Co-authored-by: Paul-Nicolas Madelaine <paul-nicolas.madelaine@ens.fr> Co-authored-by: Paul-Nicolas Madelaine <paul-nicolas.madelaine@ens.fr>