Merge `exp`, `Real.exp`, and `Complex.exp`

[eric-wieser]

We currently have at least three exponential functions. If we merge them, we will:

• maybe be able to deduplicate some lemmas
• not have to deal with namespace ambiguity between the different exps