Problem (2025ShuZhiMiMOM3p5): In non-isosceles acute-angled $\triangle ABC$, $\Omega$ is the circumcircle and $\omega$ is the nine-point circle. The tangents from $B$ and $C$ to $\Omega$ intersect at point $P$. Let $Q$ be a point on $\omega$ such that $BQ = QC$ and $Q$ is not on $BC$. Construct a circle $\Gamma$ symmetrical to $\Omega$ about $BC$, and let $\Gamma$ intersect $\omega$ at points $D$ and $E$. Let $F$ be the isogonal conjugate of $D$ with respect to $\triangle ABC$. Prove that $E$, $F$, $P$, $Q$ are concyclic.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; m1 = midpoint b c; m2 = midpoint a c; m3 = midpoint a b; n = circumcenter m1 m2 m3; p = on_tline b o b, on_tline c o c; q = on_circle n m1, on_bline b c; o1 = reflect o b c; d = on_circle o1 b, on_circle n m1; e = on_circle o1 b, on_circle n m1; f = on_aline f a c b a d, on_aline f b c a b d ? cyclic e f p q
HAGeo formalization: A B C = triangle; O = circumcenter A B C; M1 = midpoint B C; M2 = midpoint A C; M3 = midpoint A B; N = circumcenter M1 M2 M3; OB = line O B; OC = line O C; l1 = perpendicular_line B OB; l2 = perpendicular_line C OC; P = intersection l1 l2; (N) = circle_center_point N M1; l3 = perpendicular_bisector B C; Q = intersection (N) l3; BC = line B C; O1 = reflect_point_wrt_line O BC; (O1) = circle_center_point O1 B; D E = intersection (O1) (N); l4 = angle_equal1 A C B A D; l5 = angle_equal1 B C A B D; F = intersection l4 l5; Prove: concyclic E F P Q
Difficulty score: 5.5