Problem (2023PlanetCupp9): For $\triangle ABC$ with circumcircle $\Omega$, orthocenter $H$, and circumcenter $O$, line $OH$ meets $AC,AB$ at $E,F$. The circumcircle of $\triangle AHO$ meets $\Omega$ at $K$, and $KH$ extended meets $\Omega$ at $L$. With $M$ as $BC$'s midpoint, let $P\in HM$ satisfy $PE=PF$. If $PL$ meets $BC$ at $Q$, prove $QH=QO$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; e = on_line o h, on_line a c; f = on_line o h, on_line a b; o1 = circumcenter a h o; k = on_circle o1 a, on_circle o a; l = on_line k h, on_circle o a; m = midpoint b c; p = on_line h m, on_bline e f; q = on_line p l, on_line b c ? cong q h q o
HAGeo formalization: A B C = triangle; O = circumcenter A B C; H = orthocenter A B C; OH = line O H; AC = line A C; E = intersection OH AC; AB = line A B; F = intersection OH AB; O1 = circumcenter A H O; (O1) = circle_center_point O1 A; (O) = circle_center_point O A; K = intersection (O1) (O); KH = line K H; L = intersection KH (O); M = midpoint B C; HM = line H M; l1 = perpendicular_bisector E F; P = intersection HM l1; PL = line P L; BC = line B C; Q = intersection PL BC; Prove: cong Q H Q O
Difficulty score: 5.9