Problem (2022IranGOAp2): We are given an acute triangle $ABC$ with $AB\neq AC$. Let $D$ be a point of $BC$ such that $DA$ is tangent to the circumcircle of $ABC$. Let $E$ and $F$ be the circumcenters of triangles $ABD$ and $ACD$, respectively, and let $M$ be the midpoints $EF$. Prove that the line tangent to the circumcircle of $AMD$ through $D$ is also tangent to the circumcircle of $ABC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_line b c, on_tline a o a; e = circumcenter a b d; f = circumcenter a c d; m = midpoint e f; o1 = circumcenter a m d; t = on_tline d o1 d; x = foot o d t ? cong o x o a
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; OA = line O A; l1 = perpendicular_line A OA; BC = line B C; D = intersection l1 BC; E = circumcenter A B D; F = circumcenter A C D; M = midpoint E F; O1 = circumcenter A D M; O1D = line O1 D; l = perpendicular_line D O1D; X = foot O l; Prove: cong O X O A
Difficulty score: 2.7