Commit 2020-10-13 02:01 7dcaee1c

feat(archive/imo): formalize IMO 1962 problem 4 (#4518) The problem statement: Solve the equation cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1. There are a bunch of trig formulas I proved along the way; there are sort of an infinite number of trig formulas so I'm open to feedback on whether some should go in the core libraries. Also possibly some of them have a shorter proof that would render the lemma unnecessary. For what it's worth, the actual method of solution is not how a human would do it; a more intuitive human method is to simplify in terms of cos x and then solve, but I think this is simpler in Lean because it doesn't rely on solving cos x = y for several different y.