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