Problem (2020IranGOMp3): In acute-angled triangle $ABC$ ($AC > AB$), point $H$ is the orthocenter and point $M$ is the midpoint of the segment $BC$. The median $AM$ intersects the circumcircle of triangle $ABC$ at $X$. The line $CH$ intersects the perpendicular bisector of $BC$ at $E$ and the circumcircle of the triangle $ABC$ again at $F$. Point $J$ lies on circle $\omega$, passing through $X, E,$ and $F$, such that $BCHJ$ is a trapezoid ($CB \parallel HJ$). Prove that $JB$ and $EM$ meet on $\omega$.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; m = midpoint b c; o = circumcenter a b c; x = on_line a m, on_circle o a; e = on_line c h, on_bline b c; f = on_line c h, on_circle o c; o1 = circumcenter x e f; j = on_circle o1 x, on_pline h b c; k = on_line j b, on_line e m ? cyclic k x e f
HAGeo formalization: A B C = acute_triangle; H = orthocenter A B C; M = midpoint B C; AM = line A M; O = circumcenter A B C; (ABC) = circle_center_point O A; X = intersection AM (ABC); l1 = perpendicular_bisector B C; CH = line C H; E = intersection CH l1; F = intersection CH (ABC); BC = line B C; l2 = parallel_line H BC; O1 = circumcenter X E F; (EFX) = circle_center_point O1 X; J = intersection (EFX) l2; BJ = line B J; EM = line E M; K = intersection BJ EM; Prove: concyclic K X E F
Difficulty score: 3.3