Problem (2017SilkRoadp2): The quadrilateral $ABCD$ is inscribed in the circle $\omega$. The diagonals $AC$ and $BD$ intersect at the point $O$. On the segments $AO$ and $DO$, the points $E$ and $F$ are chosen, respectively. The straight line $EF$ intersects $\omega$ at the points $E_1$ and $F_1$. The circumscribed circles of the triangles $ADE$ and $BCF$ intersect the segment $EF$ at the points $E_2$ and $F_2$ respectively (assume that all the points $E, F, E_1, F_1, E_2$ and $F_2$ are different). Prove that $E_1E_2 = F_1F_2$.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; o = on_line a c, on_line b d; e = on_line a o; f = on_line d o; e1 = on_line e f, on_circum a b c; f1 = on_line e f, on_circum a b c; o2 = circumcenter a d e; o3 = circumcenter b c f; e2 = on_line e f, on_circle o2 a; f2 = on_line e f, on_circle o3 b ? cong e1 e2 f1 f2
HAGeo formalization: A B C = triangle; (ABC) = circumcircle A B C; D = on_circle (ABC); AC = line A C; BD = line B D; O = intersection AC BD; AO = line A O; E = on_line AO; DO = line D O; F = on_line DO; EF = line E F; E1 F1 = intersection EF (ABC); (ADE) = circle A D E; E2 = intersection (ADE) EF; (BCF) = circle B C F; F2 = intersection (BCF) EF; Prove: cong E1 E2 F1 F2
Difficulty score: 2.5