Problem (2021CzechAPSlovakp2): In an acute triangle $ABC$, the incircle $\omega$ touches $BC$ at $D$. Let $I_a$ be the excenter of $ABC$ opposite to $A$, and let $M$ be the midpoint of $DI_a$. Prove that the circumcircle of triangle $BMC$ is tangent to $\omega$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; i1 = excenter a b c; m = midpoint d i1; o1 = circumcenter b m c; x = on_line o1 i, on_circle o1 b ? cong i x i d
HAGeo formalization: A B C = acute_triangle; I = incenter A B C; BC = line B C; D = foot I BC; I1 = excenter A B C; M = midpoint D I1; O1 = circumcenter B C M; (O1) = circle_center_point O1 B; O1I = line O1 I; X = intersection O1I (O1); Prove: cong I X I D
Difficulty score: 2.9