Problem (2023CHNSouthEastMOg11p5): As shown in the figure, in $\vartriangle ABC$, $AB>AC$, the inscribed circle $I$ is tangent to the sides $BC$, $CA$, $AB$ at points $D$, $E$, $F$ respectively, and the straight lines $BC$ and $EF$ intersect at point $K$, $DG \perp EF$ at point $G$, ray $IG$ intersects the circumscribed circle of $\vartriangle ABC$ at point $H$. Prove that points $H$, $G$, $D$, $K$ lie on a circle.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; e = foot i c a; f = foot i a b; k = on_line b c, on_line e f; g = foot d e f; h = on_line i g, on_circum a b c ? cyclic h g d k
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; D = foot I BC; AC = line A C; E = foot I AC; AB = line A B; F = foot I AB; EF = line E F; K = intersection BC EF; G = foot D EF; GI = line G I; (ABC) = circle A B C; H = intersection GI (ABC); Prove: concyclic H G D K
Difficulty score: 2.4