Problem (2015ELMOp3): Let $\omega$ be a circle and $C$ a point outside it; distinct points $A$ and $B$ are selected on $\omega$ so that $\overline{CA}$ and $\overline{CB}$ are tangent to $\omega$. Let $X$ be the reflection of $A$ across the point $B$, and denote by $\gamma$ the circumcircle of triangle $BXC$. Suppose $\gamma$ and $\omega$ meet at $D \neq B$ and line $CD$ intersects $\omega$ at $E \neq D$. Prove that line $EX$ is tangent to the circle $\gamma$.
AlphaGeometry formalization: a b = segment; o = on_bline a b; c = on_tline a o a, on_tline b o b; x = mirror a b; o1 = circumcenter b x c; d = on_circle o a, on_circle o1 b; e = on_line c d, on_circle o a ? perp o1 x e x
HAGeo formalization: A = point; B = point; l = perpendicular_bisector A B; O = on_line l; (O) = circle_center_point O A; OA = line O A; OB = line O B; l1 = perpendicular_line A OA; l2 = perpendicular_line B OB; C = intersection l1 l2; X = reflect A B; O1 = circumcenter B X C; (O1) = circle_center_point O1 B; D = intersection (O1) (O); CD = line C D; E = intersection CD (O); EX = line E X; O1X = line O1 X; Prove: perpendicular EX O1X
Difficulty score: 2.3