Problem (2019ELMOSLp3): Let $\triangle ABC$ be an acute triangle with incenter $I$ and circumcenter $O$. The incircle touches sides $BC,CA,$ and $AB$ at $D,E,$ and $F$ respectively, and $A'$ is the reflection of $A$ over $O$. The circumcircles of $ABC$ and $A'EF$ meet at $G$, and the circumcircles of $AMG$ and $A'EF$ meet at a point $H\neq G$, where $M$ is the midpoint of $EF$. Prove that if $GH$ and $EF$ meet at $T$, then $DT\perp EF$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; o = circumcenter a b c; d = foot i b c; e = foot i a c; f = foot i a b; a1 = mirror a o; o1 = circumcenter a1 e f; g = on_circum a b c, on_circum a1 e f; m = midpoint e f; o2 = circumcenter a m g; h = on_circum a m g, on_circum a1 e f; t = on_line g h, on_line e f ? perp d t e f
HAGeo formalization: A B C = acute_triangle; I = incenter A B C; O = circumcenter 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; A1 = reflect A O; (ABC) = circle A B C; O1 = circumcenter A1 E F; (A1EF) = circle A1 E F; G = intersection (ABC) (A1EF); M = midpoint E F; O2 = circumcenter A M G; (AGM) = circle A G M; H = intersection (AGM) (A1EF); GH = line G H; EF = line E F; T = intersection GH EF; DT = line D T; Prove: perpendicular DT EF
Difficulty score: 3.5