Problem (2024VietnamTSTp5): Let incircle $(I)$ of triangle $ABC$ touch the sides $BC,CA,AB$ at $D,E,F$ respectively. Let $(O)$ be the circumcircle of $ABC$. Ray $EF$ meets $(O)$ at $M$. Tangents at $M$ and $A$ of $(O)$ meet at $S$. Tangents at $B$ and $C$ of $(O)$ meet at $T$. Line $TI$ meets $OA$ at $J$. Prove that $\angle ASJ=\angle IST$.
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; o = circumcenter a b c; m = on_line e f, on_circle o a; s = on_tline m o m, on_tline a o a; t = on_tline b o b, on_tline c o c; j = on_line t i, on_line o a ? eqangle a s s j i s s t
HAGeo formalization: A B C = triangle; 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; O = circumcenter A B C; EF = line E F; (O) = circle_center_point O A; M = intersection EF (O); OM = line O M; OA = line O A; l1 = perpendicular_line M OM; l2 = perpendicular_line A OA; S = intersection l1 l2; OB = line O B; OC = line O C; l3 = perpendicular_line B OB; l4 = perpendicular_line C OC; T = intersection l3 l4; TI = line T I; J = intersection TI OA; Prove: equal_angle A S J I S T
Difficulty score: 5.8