Problem (2016USATSTSTp6): Let $ABC$ be a triangle with incenter $I$, and whose incircle is tangent to $\overline{BC}$, $\overline{CA}$, $\overline{AB}$ at $D$, $E$, $F$, respectively. Let $K$ be the foot of the altitude from $D$ to $\overline{EF}$. Suppose that the circumcircle of $\triangle AIB$ meets the incircle at two distinct points $C_1$ and $C_2$, while the circumcircle of $\triangle AIC$ meets the incircle at two distinct points $B_1$ and $B_2$. Prove that the radical axis of the circumcircles of $\triangle BB_1B_2$ and $\triangle CC_1C_2$ passes through the midpoint $M$ of $\overline{DK}$.
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; k = foot d e f; o1 = circumcenter a i b; c1 = on_circle o1 a, on_circle i d; c2 = on_circle o1 a, on_circle i d; o2 = circumcenter a i c; b1 = on_circle o2 a, on_circle i d; b2 = on_circle o2 a, on_circle i d; o3 = circumcenter b b1 b2; o4 = circumcenter c c1 c2; p1 = on_circle o3 b, on_circle o4 c; p2 = on_circle o3 b, on_circle o4 c; m = midpoint d k ? coll m p1 p2
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; D = foot I BC; (I) = circle_center_point I D; AC = line A C; E = foot I AC; AB = line A B; F = foot I AB; EF = line E F; K = foot D EF; O1 = circumcenter A I B; (ABI) = circle_center_point O1 A; C1 C2 = intersection (ABI) (I); O2 = circumcenter A I C; (ACI) = circle_center_point O2 A; B1 B2 = intersection (ACI) (I); M = midpoint D K; O3 = circumcenter B B1 B2; (BB1B2) = circle_center_point O3 B; O4 = circumcenter C C1 C2; (CC1C2) = circle_center_point O4 C; P1 P2 = intersection (BB1B2) (CC1C2); Prove: collinear M P1 P2
Difficulty score: 5.4