Problem (2016EGMOp2): Let $ABCD$ be a cyclic quadrilateral, and let diagonals $AC$ and $BD$ intersect at $X$.Let $C_1,D_1$ and $M$ be the midpoints of segments $CX,DX$ and $CD$, respecctively. Lines $AD_1$ and $BC_1$ intersect at $Y$, and line $MY$ intersects diagonals $AC$ and $BD$ at different points $E$ and $F$, respectively. Prove that line $XY$ is tangent to the circle through $E,F$ and $X$.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; x = on_line a c, on_line b d; c1 = midpoint c x; d1 = midpoint d x; m = midpoint c d; y = on_line a d1, on_line b c1; e = on_line a c, on_line m y; f = on_line b d, on_line m y; o1 = circumcenter e f x ? perp o1 x 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; X = intersection AC BD; C1 = midpoint C X; D1 = midpoint D X; M = midpoint C D; AD1 = line A D1; BC1 = line B C1; Y = intersection AD1 BC1; MY = line M Y; E = intersection MY AC; F = intersection MY BD; XY = line X Y; O1 = circumcenter E F X; O1X = line O1 X; Prove: perpendicular O1X XY
Difficulty score: 2.6