x y : ℝ
⊢ ↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)
x y : ℝ
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x
rw [← ofReal_inj]
no goals
x y : ℝ
⊢ ↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)
simp [sinh_three_mul]