Problem (2020IranGOMp4): Triangle $ABC$ is given. An arbitrary circle with center $J$, passing through $B$ and $C$, intersects the sides $AC$ and $AB$ at $E$ and $F$, respectively. Let $X$ be a point such that triangle $FXB$ is similar to triangle $EJC$ (with the same order) and the points $X$ and $C$ lie on the same side of the line $AB$. Similarly, let $Y$ be a point such that triangle $EYC$ is similar to triangle $FJB$ (with the same order) and the points $Y$ and $B$ lie on the same side of the line $AC$. Prove that the line $XY$ passes through the orthocenter of the triangle $ABC$.
AlphaGeometry formalization: a b c = triangle; j = on_bline b c; e = on_line a c, on_circle j b; f = on_line a b, on_circle j b; h = orthocenter a b c; x = on_aline x b f j e c, on_aline x f b j c e; y = on_aline y e c j b f, on_aline y c e j f b ? coll x y h
HAGeo formalization: A B C = triangle; l = perpendicular_bisector B C; J = on_line l; (J) = circle_center_point J B; AC = line A C; E = intersection (J) AC; AB = line A B; F = intersection (J) AB; l1 = angle_equal1 B F J E C; l2 = angle_equal1 F B J C E; X = intersection l1 l2; l3 = angle_equal1 E C J B F; l4 = angle_equal1 C E J F B; Y = intersection l3 l4; H = orthocenter A B C; Prove: collinear H X Y
Difficulty score: 3.9