Problem (2011CHNWesternMOp7): In triangle $ABC$ with $AB>AC$ and incenter $I$, the incircle touches $BC,CA,AB$ at $D,E,F$ respectively. $M$ is the midpoint of $BC$, and the altitude at $A$ meets $BC$ at $H$. Ray $AI$ meets lines $DE$ and $DF$ at $K$ and $L$, respectively. Prove that the points $M,L,H,K$ are concyclic.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; e = foot i a c; f = foot i a b; m = midpoint b c; h = foot a b c; k = on_line a i, on_line d e; l = on_line a i, on_line d f ? cyclic m l h 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; M = midpoint B C; H = foot A BC; AI = line A I; DE = line D E; K = intersection AI DE; DF = line D F; L = intersection AI DF; Prove: concyclic M L H K
Difficulty score: 2.2