Commit 2023-01-18 07:04 6890b009

feat(archive/imo/imo2019_q2): IMO 2019 Q2 (#17993) Add an IMO geometry problem to the mathlib archive. The module doc string discusses the conventions followed to translate the informal statement to a formal one (which should probably end up somewhere more generally discussing conventions for formal statements of olympiad problems, but it seems reasonable to have it here for now). This formalization uses a structure describing a configuration satisfying the conditions of the problem, to build up information gradually through many lemmas without needing to pass lots of hypotheses around (and to handle explicitly the symmetry in the configuration of the problem), which seems likely to be a convenient way to handle many olympiad geometry solutions.