x y : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)
x y : ℝ
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
rw [← ofReal_inj]
no goals
x y : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)
simp [cosh_three_mul]