feat(data/complex): norm_cast lemmas (#4405)
Mark various existing lemmas such as `abs_of_real` and `of_real_exp`
as `norm_cast` lemmas so that `norm_cast` and related tactics can
handle expressions involving those functions, and add lemmas
`of_real_prod` and `of_real_sum` to allow those tactics to work with
sums and products involving coercions from real to complex.
