Problem (2021EGMOp4): Let $ABC$ be a triangle with incenter $I$ and let $D$ be an arbitrary point on the side $BC$. Let the line through $D$ perpendicular to $BI$ intersect $CI$ at $E$. Let the line through $D$ perpendicular to $CI$ intersect $BI$ at $F$. Prove that the reflection of $A$ across the line $EF$ lies on the line $BC$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = on_line b c; e = on_line i c, on_tline d b i; f = on_line i b, on_tline d c i; a1 = reflect a e f ? coll b c a1
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; D = on_line BC; BI = line B I; l1 = perpendicular_line D BI; CI = line C I; E = intersection l1 CI; l2 = perpendicular_line D CI; F = intersection l2 BI; EF = line E F; A1 = reflect_point_wrt_line A EF; Prove: collinear A1 B C
Difficulty score: 2.8