x y : ℂ
⊢ cosh (x * I * I) = cosh x
x y : ℂ
⊢ cos (x * I) = cosh x
rw [← cosh_mul_I]
x y : ℂ
⊢ cosh (x * I ^ 2) = cosh x
x y : ℂ
⊢ cosh (x * I * I) = cosh x
ring_nf
no goals
x y : ℂ
⊢ cosh (x * I ^ 2) = cosh x
simp