Problem (2016IranGOMp5): Let the circles $\omega$ and $\omega'$ intersect in points $A$ and $B$. The tangent to circle $\omega$ at $A$ intersects $\omega'$ at $C$ and the tangent to circle $\omega'$ at $A$ intersects $\omega$ at $D$. Suppose that the internal bisector of $\angle CAD$ intersects $\omega$ and $\omega'$ at $E$ and $F$, respectively, and the external bisector of $\angle CAD$ intersects $\omega$ and $\omega'$ at $X$ and $Y$, respectively. Prove that the perpendicular bisector of $XY$ is tangent to the circumcircle of triangle $BEF$.
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; c = on_circle o2 a, on_tline a o1 a; d = on_circle o1 a, on_tline a o2 a; r = angle_bisector c a d; s = on_tline a a r; e = on_line a r, on_circle o1 a; f = on_line a r, on_circle o2 a; x = on_line a s, on_circle o1 a; y = on_line a s, on_circle o2 a; o3 = circumcenter b e f; m = midpoint x y; t = on_bline x y, on_pline o3 x y ? cyclic b e f t
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; O1A = line O1 A; l1 = perpendicular_line A O1A; C = intersection l1 (O2); O2A = line O2 A; l2 = perpendicular_line A O2A; D = intersection l2 (O1); l3 = angle_bisector C A D; E = intersection l3 (O1); F = intersection l3 (O2); l4 = angle_exbisector C A D; X = intersection l4 (O1); Y = intersection l4 (O2); l5 = perpendicular_bisector X Y; O3 = circumcenter B E F; XY = line X Y; l6 = parallel_line O3 XY; T = intersection l5 l6; Prove: concyclic B E F T
Difficulty score: 2.3