x y : ℂ
⊢ sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x
x y : ℂ
⊢ sinh (2 * x) = 2 * sinh x * cosh x
rw [two_mul, sinh_add]
no goals
x y : ℂ
⊢ sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x
ring