case h.e'_2.h.e'_1
x y z : ℂ
⊢ z = ↑z.re + ↑z.im * I
x y z : ℂ
⊢ cos z = cos ↑z.re * cosh ↑z.im - sin ↑z.re * sinh ↑z.im * I
convert cos_add_mul_I z.re z.im
no goals
case h.e'_2.h.e'_1
x y z : ℂ
⊢ z = ↑z.re + ↑z.im * I
exact (re_add_im z).symm