Problem (2016RMMSLG1): Two circles, $\omega_1$ and $\omega_2$, centred at $O_1$ and $O_2$, respectively, meet at points $A$ and $B$. A line through $B$ meets $\omega_1$ again at $C$, and $\omega_2$ again at $D$. The tangents to $\omega_1$ and $\omega_2$ at $C$ and $D$, respectively, meet at $E$, and the line $AE$ meets the circle $\omega$ through $A, O_1, O_2$ again at $F$. Prove that the length of the segment $EF$ is equal to the diameter of $\omega$.
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; c = on_circle o1 a; d = on_line b c, on_circle o2 a; e = on_tline c o1 c, on_tline d o2 d; o_w = circumcenter a o1 o2; f = on_line a e, on_circle o_w a; f1 = mirror f o_w ? cong e f f f1
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; C = on_circle (O1); BC = line B C; D = intersection BC (O2); O1C = line O1 C; O2D = line O2 D; l1 = perpendicular_line C O1C; l2 = perpendicular_line D O2D; E = intersection l1 l2; O_w = circumcenter A O1 O2; AE = line A E; (O_w) = circle_center_point O_w A; F = intersection AE (O_w); F1 = reflect_point_wrt_point F O_w; Prove: cong E F F F1
Difficulty score: 4.2