Problem (2023SerbiaMOp6): Given is a triangle $ABC$ with incenter $I$ and circumcircle $\omega$. The incircle is tangent to $BC$ at $D$. The perpendicular at $I$ to $AI$ meets $AB, AC$ at $E, F$ and the circle $(AEF)$ meets $\omega$ and $AI$ at $G, H$. The tangent at $G$ to $\omega$ meets $BC$ at $J$ and $AJ$ meets $\omega$ at $K$. Prove that $(DJK)$ and $(GIH)$ are tangent to each other.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; o = circumcenter a b c; d = foot i b c; e = on_line a b, on_tline i a i; f = on_line a c, on_tline i a i; o1 = circumcenter a e f; g = on_circle o1 a, on_circle o a; h = on_circle o1 a, on_line a i; j = on_tline g o g, on_line b c; k = on_line a j, on_circle o a; o3 = circumcenter d j k; o4 = circumcenter g i h; t = on_circle o4 i, on_circle o3 d ? coll t o4 o3
HAGeo formalization: A B C = triangle; I = incenter A B C; O = circumcenter A B C; BC = line B C; D = foot I BC; AB = line A B; AI = line A I; l1 = perpendicular_line I AI; E = intersection AB l1; AC = line A C; F = intersection AC l1; O1 = circumcenter A E F; (O1) = circle_center_point O1 A; (O) = circle_center_point O A; G = intersection (O1) (O); AI = line A I; H = intersection (O1) AI; OG = line O G; l2 = perpendicular_line G OG; J = intersection l2 BC; AJ = line A J; K = intersection AJ (O); O3 = circumcenter D J K; O4 = circumcenter G I H; (GIH) = circle_center_point O4 I; (DJK) = circle_center_point O3 D; T = intersection (GIH) (DJK); Prove: collinear T O4 O3
Difficulty score: 4.2