Problem (2020IranTSTp9): Given a triangle $ABC$ with circumcircle $\Gamma$. Points $E$ and $F$ are the foot of angle bisectors of $B$ and $C$, $I$ is incenter and $K$ is the intersection of $AI$ and $EF$. Suppose that $T$ be the midpoint of arc $BAC$. Circle $\Gamma$ intersects the $A$-median and circumcircle of $AEF$ for the second time at $X$ and $S$. Let $S'$ be the reflection of $S$ across $AI$ and $J$ be the second intersection of circumcircle of $AS'K$ and $AX$. Prove that quadrilateral $TJIX$ is cyclic.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; i = incenter a b c; e = on_line a c, angle_bisector c b a; f = on_line a b, angle_bisector b c a; k = on_line a i, on_line e f; t = on_circle o a, on_bline b c; m = midpoint b c; x = on_line a m, on_circle o a; o1 = circumcenter a e f; s = on_circle o1 a, on_circle o a; s1 = reflect s a i; o2 = circumcenter a s1 k; j = on_line a x, on_circle o2 a ? cyclic t j i x
HAGeo formalization: A B C = triangle; O = circumcenter A B C; I = incenter A B C; AC = line A C; l1 = angle_bisector C B A; E = intersection AC l1; AB = line A B; l2 = angle_bisector B C A; F = intersection AB l2; AI = line A I; EF = line E F; K = intersection AI EF; (O) = circle_center_point O A; l3 = perpendicular_bisector B C; T = intersection (O) l3; M = midpoint B C; AM = line A M; X = intersection AM (O); O1 = circumcenter A E F; (O1) = circle_center_point O1 A; S = intersection (O1) (O); S1 = reflect_point_wrt_line S AI; O2 = circumcenter A S1 K; AX = line A X; (O2) = circle_center_point O2 A; J = intersection AX (O2); Prove: concyclic T J I X
Difficulty score: 5.3