x y : ℂ
⊢ (exp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).re = Real.exp x.re * Real.cos x.im
x y : ℂ
⊢ (exp x).re = Real.exp x.re * Real.cos x.im
rw [exp_eq_exp_re_mul_sin_add_cos]
no goals
x y : ℂ
⊢ (exp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).re = Real.exp x.re * Real.cos x.im
simp [exp_ofReal_re, cos_ofReal_re]