Problem (2019USATSTSTp5): Let $ABC$ be an acute triangle with orthocenter $H$ and circumcircle $\Gamma$. A line through $H$ intersects segments $AB$ and $AC$ at $E$ and $F$, respectively. Let $K$ be the circumcenter of $\triangle AEF$, and suppose line $AK$ intersects $\Gamma$ again at a point $D$. Prove that line $HK$ and the line through $D$ perpendicular to $\overline{BC}$ meet on $\Gamma$.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; o = circumcenter a b c; e = on_line a b; f = on_line a c, on_line e h; k = circumcenter a e f; d = on_line a k, on_circum a b c; p = on_line h k, on_tline d b c ? cyclic p a b c
HAGeo formalization: A B C = acute_triangle; H = orthocenter A B C; O = circumcenter A B C; (ABC) = circle A B C; AB = line A B; E = on_line AB; EH = line E H; AC = line A C; F = intersection EH AC; K = circumcenter A E F; AK = line A K; D = intersection AK (ABC); BC = line B C; l1 = perpendicular_line D BC; HK = line H K; X = intersection l1 HK; Prove: concyclic X A B C
Difficulty score: 3.5