Problem (MouseMOp3): In acute $\triangle ABC$, let $X_1,X_2$ be the 1st and 2nd Fermat points. For $S$ on the circumcircle of $\triangle AX_1X_2$, line $AS$ meets the circumcircle of $\triangle BSC$ at $T$. Prove that the Euler lines of $\triangle ABC$ and $\triangle TBC$ are parallel.
AlphaGeometry formalization: a b c = triangle; d1 = eq_triangle b c; e1 = eq_triangle c a; f1 = eq_triangle a b; x1 = on_line a d1, on_line b e1; d2 = eq_triangle c b; e2 = eq_triangle a c; f2 = eq_triangle b a; x2 = on_line a d2, on_line b e2; o1 = circumcenter a x1 x2; s = on_circle o1 a; o2 = circumcenter b s c; t = on_line a s, on_circle o2 b; o = circumcenter a b c; h = orthocenter a b c; h1 = orthocenter t b c ? para o h o2 h1
HAGeo formalization: A B C = triangle; D1 = equilateral_triangle B C; E1 = equilateral_triangle C A; F1 = equilateral_triangle A B; AD1 = line A D1; BE1 = line B E1; X1 = intersection AD1 BE1; D2 = equilateral_triangle C B; E2 = equilateral_triangle A C; F2 = equilateral_triangle B A; AD2 = line A D2; BE2 = line B E2; X2 = intersection AD2 BE2; O1 = circumcenter A X1 X2; (O1) = circle_center_point O1 A; S = on_circle (O1); O2 = circumcenter B S C; AS = line A S; (O2) = circle_center_point O2 B; T = intersection AS (O2); O = circumcenter A B C; H = orthocenter A B C; H1 = orthocenter T B C; OH = line O H; O2H1 = line O2 H1; Prove: parallel OH O2H1
Difficulty score: 6.4