simp only [Real.cos_two_mul, cos_three_mul, altFormula]
x : ℝ
⊢ (x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 - 1) / 4 = altFormula x
x : ℝ
⊢ (x.cos ^ 2 + (2 * x.cos ^ 2 - 1) ^ 2 + (4 * x.cos ^ 3 - 3 * x.cos) ^ 2 - 1) / 4 =
    x.cos * (x.cos ^ 2 - 1 / 2) * (4 * x.cos ^ 3 - 3 * x.cos)