mathlib3

348b41d4 - chore(archive/imo/imo1994_q1): tidy a bit (#13266)