rw [ProblemEquation, ← cos_sum_equiv, div_eq_zero_iff, sub_eq_zero]
x : ℝ
⊢ ProblemEquation x ↔ altFormula x = 0
x : ℝ
⊢ x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 = 1 ↔ x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 = 1 ∨ 4 = 0