Problem (2019GOTEEMp6): Let $ABC$ be a scalene triangle with circumcircle $\omega$ and circumcenter $O$. Let $D$ be a point on $\overline{BC}$ such that $\angle BAD = \angle CAD$. The tangent to $\omega$ at $A$ meets $\overline{BC}$ at $T$. Suppose that the circumcircles of $\triangle ABC$ and $\triangle ADO$ intersect again at $X$, and the circumcircles of $\triangle DOT$ and $\triangle AXT$ intersect again at $M$. Prove that $MX$ is tangent to the circumcircle of $\triangle ADO$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_line b c, angle_bisector b a c; t = on_line b c, on_tline a o a; o1 = circumcenter a o d; x = on_circle o a, on_circle o1 a; m = on_circum d o t, on_circum a x t ? perp o1 x x m
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (O) = circle_center_point O A; l1 = angle_bisector B A C; BC = line B C; D = intersection BC l1; OA = line O A; l2 = perpendicular_line A OA; T = intersection l2 BC; O1 = circumcenter A O D; (ADO) = circle_center_point O1 A; X = intersection (O) (ADO); (DOT) = circle D O T; (ATX) = circle A T X; M = intersection (DOT) (ATX); MX = line M X; O1X = line O1 X; Prove: perpendicular O1X MX
Difficulty score: 3.6