Problem (2019ELMOSLp1): Let $ABC$ be an acute triangle with orthocenter $H$ and circumcircle $\Gamma$. Let $BH$ intersect $AC$ at $E$, and let $CH$ intersect $AB$ at $F$. Let $AH$ intersect $\Gamma$ again at $P \neq A$. Let $PE$ intersect $\Gamma$ again at $Q \neq P$. Prove that $BQ$ bisects segment $\overline{EF}$.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; e = on_line a c, on_line b h; f = on_line a b, on_line c h; p = on_line a h, on_circum a b c; q = on_line p e, on_circum a b c; m = on_line b q, on_line e f ? midp m e f
HAGeo formalization: A B C = acute_triangle; H = orthocenter A B C; BH = line B H; AC = line A C; E = intersection BH AC; CH = line C H; AB = line A B; F = intersection CH AB; AH = line A H; (ABC) = circle A B C; P = intersection AH (ABC); EP = line E P; Q = intersection EP (ABC); EF = line E F; BQ = line B Q; M = intersection EF BQ; Prove: midpoint M E F
Difficulty score: 3.1