Problem (2017ARMOg9p2): $ABCD$ is an isosceles trapezoid with $BC || AD$. A circle $\omega$ passing through $B$ and $C$ intersects the side $AB$ and the diagonal $BD$ at points $X$ and $Y$ respectively. Tangent to $\omega$ at $C$ intersects the line $AD$ at $Z$. Prove that the points $X$, $Y$, and $Z$ are collinear.
AlphaGeometry formalization: d a b c = eq_trapezoid; o = on_bline b c; x = on_line a b, on_circle o b; y = on_line b d, on_circle o b; z = on_line a d, on_tline c o c ? coll x y z
HAGeo formalization: A B C D = isos_trapezoid; l = perpendicular_bisector B C; O = on_line l; (O) = circle_center_point O B; AB = line A B; X = intersection AB (O); BD = line B D; Y = intersection BD (O); OC = line O C; l1 = perpendicular_line C OC; AD = line A D; Z = intersection l1 AD; Prove: collinear X Y Z
Difficulty score: 1.6