Problem (2018IranGOMp3): Let $\omega_1,\omega_2$ be two circles with centers $O_1$ and $O_2$, respectively. These two circles intersect each other at points $A$ and $B$. Line $O_1B$ intersects $\omega_2$ for the second time at point $C$, and line $O_2A$ intersects $\omega_1$ for the second time at point $D$ . Let $X$ be the second intersection of $AC$ and $\omega_1$. Also $Y$ is the second intersection point of $BD$ and $\omega_2$. Prove that $CX = DY$ .
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; c = on_line o1 b, on_circle o2 a; d = on_line o2 a, on_circle o1 a; x = on_line a c, on_circle o1 a; y = on_line b d, on_circle o2 a ? cong c x d y
HAGeo formalization: A = point; B = point; l = perpendicular_bisector A B; O1 = on_line l; O2 = on_line l; (O1) = circle_center_point O1 A; (O2) = circle_center_point O2 A; BO1 = line B O1; C = intersection BO1 (O2); AO2 = line A O2; D = intersection AO2 (O1); AC = line A C; X = intersection AC (O1); BD = line B D; Y = intersection BD (O2); Prove: cong C X D Y
Difficulty score: 2.9