Problem (2021USATSTSTp1): Let $ABCD$ be a quadrilateral inscribed in a circle with center $O$. Points $X$ and $Y$ lie on sides $AB$ and $CD$, respectively. Suppose the circumcircles of $ADX$ and $BCY$ meet line $XY$ again at $P$ and $Q$, respectively. Show that $OP=OQ$.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; o = circumcenter a b c; x = on_line a b; y = on_line c d; o1 = circumcenter a d x; p = on_line x y, on_circle o1 a; o2 = circumcenter b c y; q = on_line x y, on_circle o2 b ? cong o p o q
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); O = circumcenter A B C; AB = line A B; X = on_line AB; CD = line C D; Y = on_line CD; XY = line X Y; O1 = circumcenter A D X; (O1) = circle_center_point O1 A; P = intersection XY (O1); O2 = circumcenter B C Y; (O2) = circle_center_point O2 B; Q = intersection XY (O2); Prove: cong O P O Q
Difficulty score: 2.7