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