Theorem: Imo1962P4.cos_sum_equiv (Compfiles/Imo1962P4.lean)

State before:
x : ℝ
⊢ (x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 - 1) / 4 = altFormula x
Tactic:
simp only [Real.cos_two_mul, cos_three_mul, altFormula]
State after:
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)

State before:
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)
Tactic:
ring
State after:
no goals