Problem (2020CGMOp7): Let $O$ be the circumcenter of triangle $\triangle ABC$, where $\angle BAC=120^{\circ}$. The tangent at $A$ to $(ABC)$ meets the tangents at $B,C$ at $(ABC)$ at points $P,Q$ respectively. Let $H,I$ be the orthocenter and incenter of $\triangle OPQ$ respectively. Define $M,N$ as the midpoints of arc $\overarc{BAC}$ and $OI$ respectively, and let $MN$ meet $(ABC)$ again at $D$. Prove that $AD$ is perpendicular to $HI$.
AlphaGeometry formalization: b c x = ieq_triangle; o = circumcenter b c x; a = on_circle o x; p = on_tline a o a, on_tline b o b; q = on_tline a o a, on_tline c o c; h = orthocenter o p q; i = incenter o p q; m = on_bline b c, on_circle o a; n = midpoint o i; d = on_line m n, on_circle o a ? perp a d h i
HAGeo formalization: B C X = equilateral_triangle; O = circumcenter B C X; (O) = circle_center_point O X; A = on_circle (O); OA = line O A; OB = line O B; OC = line O C; ta = perpendicular_line A OA; tb = perpendicular_line B OB; tc = perpendicular_line C OC; P = intersection ta tb; Q = intersection ta tc; H = orthocenter O P Q; I = incenter O P Q; l1 = perpendicular_bisector B C; M = intersection l1 (O); N = midpoint O I; MN = line M N; D = intersection MN (O); AD = line A D; HI = line H I; Prove: perpendicular AD HI
Difficulty score: 3.6