Problem (2022IranGOMp5): Let $ABCD$ be a quadrilateral inscribed in a circle $\omega$ with center $O$. Let $P$ be the intersection of two diagonals $AC$ and $BD$. Let $Q$ be a point lying on the segment $OP$. Let $E$ and $F$ be the orthogonal projections of $Q$ on the lines $AD$ and $BC$, respectively. The points $M$ and $N$ lie on the circumcircle of triangle $QEF$ such that $QM \parallel AC$ and $QN \parallel BD$. Prove that the two lines $ME$ and $NF$ meet on the perpendicular bisector of segment $CD$.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; o = circumcenter a b c; p = on_line a c, on_line b d; q = on_line o p; e = foot q a d; f = foot q b c; o1 = circumcenter q e f; m = on_circle o1 q, on_pline q a c; n = on_circle o1 q, on_pline q b d; x = on_line m e, on_line n f ? cong x c x d
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); O = circumcenter A B C; AC = line A C; BD = line B D; P = intersection AC BD; OP = line O P; Q = on_line OP; AD = line A D; BC = line B C; E = foot Q AD; F = foot Q BC; O1 = circumcenter Q E F; (O1) = circle_center_point O1 Q; l1 = parallel_line Q AC; M = intersection (O1) l1; l2 = parallel_line Q BD; N = intersection (O1) l2; ME = line M E; NF = line N F; X = intersection ME NF; Prove: cong X C X D
Difficulty score: 4.5