Problem (2023KoMaLA844): The inscribed circle of triangle $ABC$ is tangent to sides $BC$, $AC$ and $AB$ at points $D$, $E$ and $F$, respectively. Let $E'$ be the reflection of point $E$ across line $DF$, and $F'$ be the reflection of point $F$ across line $DE$. Let line $EF$ intersect the circumcircle of triangle $AE'F'$ at points $X$ and $Y$. Prove that $DX=DY$.
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; e1 = reflect e d f; f1 = reflect f d e; o1 = circumcenter a e1 f1; x = on_line e f, on_circle o1 a; y = on_line e f, on_circle o1 a ? cong d x d y
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; DF = line D F; E1 = reflect_point_wrt_line E DF; DE = line D E; F1 = reflect_point_wrt_line F DE; EF = line E F; O1 = circumcenter A E1 F1; (O1) = circle_center_point O1 A; X Y = intersection EF (O1); Prove: cong D X D Y
Difficulty score: 3.0