x y : ℝ
⊢ ↑(sinh (x + y)) = ↑(sinh x * cosh y + cosh x * sinh y)
x y : ℝ
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh y
rw [← ofReal_inj]
no goals
x y : ℝ
⊢ ↑(sinh (x + y)) = ↑(sinh x * cosh y + cosh x * sinh y)
simp [sinh_add]