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

State before:
x : ℝ
⊢ ProblemEquation x ↔ altFormula x = 0
Tactic:
rw [ProblemEquation, ← cos_sum_equiv, div_eq_zero_iff, sub_eq_zero]
State after:
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

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