x y : ℂ
⊢ (exp x - exp (-x)) * (exp y + exp (-y)) + (exp x + exp (-x)) * (exp y - exp (-y)) =
    2 * (exp x * exp y - exp (-x) * exp (-y))
x y : ℂ
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh y
rw [← mul_right_inj' (two_ne_zero' ℂ), two_sinh, exp_add, neg_add, exp_add, eq_comm, mul_add, ←
  mul_assoc, two_sinh, mul_left_comm, two_sinh, ← mul_right_inj' (two_ne_zero' ℂ), mul_add,
  mul_left_comm, two_cosh, ← mul_assoc, two_cosh]
no goals
x y : ℂ
⊢ (exp x - exp (-x)) * (exp y + exp (-y)) + (exp x + exp (-x)) * (exp y - exp (-y)) =
    2 * (exp x * exp y - exp (-x) * exp (-y))
exact sinh_add_aux