IMO 1962 Q4 #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Solve the equation
cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1.
Since Lean does not have a concept of "simplest form", we just express what is
in fact the simplest form of the set of solutions, and then prove it equals the set of solutions.
Someday, when there is a Grobner basis tactic, try to automate this proof. (A little tricky --
the ideals are not the same but their Jacobson radicals are.)