Problem (ShuZhiMiGeo109): For $\triangle ABC$ with incenter $I$, excenters $I_a,I_b,I_c$, and $\triangle I_aI_bI_c$'s circumcenter $B_e$, construct circle with diameter $IB_e$. Lines through $I\parallel BC,CA,AB$ meet this circle at $D,E,F$. Prove $\triangle DEF$'s incenter is $\triangle ABC$'s Nagel point.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; i_a = excenter a b c; i_b = excenter b c a; i_c = excenter c a b; b_e = circumcenter i_a i_b i_c; d = on_pline i b c, on_dia i b_e; e = on_pline i c a, on_dia i b_e; f = on_pline i a b, on_dia i b_e; d1 = foot i_a b c; e1 = foot i_b a c; n1 = on_line a d1, on_line b e1 ? eqangle d e e n1 n1 e e f
HAGeo formalization: A B C = triangle; I = incenter A B C; Ia = excenter A B C; Ib = excenter B C A; Ic = excenter C A B; Be = circumcenter Ia Ib Ic; BC = line B C; AC = line A C; AB = line A B; l1 = parallel_line I BC; (IBe) = circle_diameter I Be; D = intersection l1 (IBe); l2 = parallel_line I AC; E = intersection l2 (IBe); l3 = parallel_line I AB; F = intersection l3 (IBe); D1 = foot Ia BC; E1 = foot Ib AC; AD1 = line A D1; BE1 = line B E1; N1 = intersection AD1 BE1; Prove: equal_angle D E N1 N1 E F
Difficulty score: 5.5