Problem (2023CHNWesternMOp6): As shown in the figure, let point $E$ be the intersection of the diagonals $AC$ and $BD$ of the cyclic quadrilateral $ABCD$. The circumcenter of triangle $ABE$ is denoted as $K$. Point $X$ is the reflection of point $B$ with respect to the line $CD$, and point $Y$ is the point on the plane such that quadrilateral $DKEY$ is a parallelogram. Prove that the points $D,E,X,Y$ are concyclic.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; e = on_line a c, on_line b d; k = circumcenter a b e; x = reflect b c d; y = parallelogram d k e y ? cyclic d e x y
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); AC = line A C; BD = line B D; E = intersection AC BD; K = circumcenter A B E; CD = line C D; X = reflect_point_wrt_line B CD; Y = parallelogram D K E; Prove: concyclic D E X Y
Difficulty score: 1.9