no goals
x y : ℂ
⊢ cos (x + y) = cos x * cos y - sin x * sin y
rw [← cosh_mul_I, add_mul, cosh_add, cosh_mul_I, cosh_mul_I, sinh_mul_I, sinh_mul_I,
  mul_mul_mul_comm, I_mul_I, mul_neg_one, sub_eq_add_neg]