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