Problem (ShuZhiMiGeo489): In non-isosceles acute $\triangle ABC$ with circumcenter $O$ and incenter $I$, let $D,E,F$ be the contact points of incircle $\odot I$ with $BC,CA,AB$. Take $H$ as $D$'s reflection over $EF$. Extend $OI$ to meet $\odot O$ at $M$, and $IO$ to meet $BC$ at $T$. Let $AT$ meet $\odot O$ at $Q$, and $MA$ extended meet $\odot QMH$ at $Y$. Prove $Y$'s reflection over $EF$ lies on $BC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; i = incenter a b c; d = foot i b c; e = foot i a c; f = foot i a b; h = reflect d e f; m = on_line o i, on_circle o a; t = on_line i o, on_line b c; q = on_line a t, on_circle o a; o1 = circumcenter q m h; y = on_line m a, on_circle o1 q; y1 = reflect y e f ? coll y1 b c
HAGeo formalization: A B C = triangle; O = circumcenter A B C; I = incenter A B C; BC = line B C; AC = line A C; AB = line A B; D = foot I BC; E = foot I AC; F = foot I AB; EF = line E F; H = reflect_point_wrt_line D EF; OI = line O I; (O) = circle_center_point O A; M = intersection OI (O); T = intersection OI BC; AT = line A T; Q = intersection AT (O); O1 = circumcenter Q M H; MA = line M A; (O1) = circle_center_point O1 Q; Y = intersection MA (O1); Y1 = reflect_point_wrt_line Y EF; Prove: collinear Y1 B C
Difficulty score: 5.9