Problem (2025XinXingSpringMOp5): In non-isosceles acute $\triangle ABC$ with circumcenter $O$ and orthocenter $H$, let $EF\parallel AO$ through $H$ meet $AC,AB$ at $E,F$. The second intersection of $(ABC)$ and $(AEF)$ is $G$, with $AG\cap BC=J$. Let $H'$ be the orthocenter of $\triangle AEF$, $K$ lie on $(AEF)$ with $HA=HK$, $L$ be $A$'s antipodal point on $(AEF)$, and $X=AG\cap HH'$. Prove the intersection of $LX$ and $JK$ lies on $(AEF)$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; e = on_pline h a o, on_line a c; f = on_pline h a o, on_line a b; o1 = circumcenter a e f; g = on_circle o a, on_circle o1 a; j = on_line a g, on_line b c; h1 = orthocenter a e f; k = on_circle o1 a, on_circle h a; l = mirror a o1; x = on_line a g, on_line h h1; y = on_line l x, on_line j k ? cyclic y a e f
HAGeo formalization: A B C = triangle; O = circumcenter A B C; H = orthocenter A B C; AO = line A O; l1 = parallel_line H AO; AC = line A C; E = intersection l1 AC; AB = line A B; F = intersection l1 AB; O1 = circumcenter A E F; (O) = circle_center_point O A; (O1) = circle_center_point O1 A; G = intersection (O) (O1); AG = line A G; BC = line B C; J = intersection AG BC; H1 = orthocenter A E F; (H) = circle_center_point H A; K = intersection (O1) (H); L = reflect_point_wrt_point A O1; HH1 = line H H1; X = intersection AG HH1; LX = line L X; JK = line J K; Y = intersection LX JK; Prove: concyclic Y A E F
Difficulty score: 6.0