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