Problem (2022IranGOAp3): In triangle $ABC$ $(\angle A\neq 90^\circ)$, let $O$, $H$ be the circumcenter and the foot of the altitude from $A$ respectively. Suppose $M$, $N$ are the midpoints of $BC$, $AH$ respectively. Let $D$ be the intersection of $AO$ and $BC$ and let $H'$ be the reflection of $H$ about $M$. Suppose that the circumcircle of $OH'D$ intersects the circumcircle of $BOC$ at $E$. Prove that $NO$ and $AE$ are concurrent on the circumcircle of $BOC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = foot a b c; m = midpoint b c; n = midpoint a h; d = on_line a o, on_line b c; h1 = mirror h m; o1 = circumcenter o h1 d; o2 = circumcenter b o c; e = on_circle o1 o, on_circle o2 o; p = on_line n o, on_line a e ? cyclic p b o c
HAGeo formalization: A B C = triangle; O = circumcenter A B C; BC = line B C; H = foot A BC; M = midpoint B C; N = midpoint A H; AO = line A O; D = intersection AO BC; H1 = reflect H M; O1 = circumcenter O H1 D; O2 = circumcenter B O C; (DH1O) = circle_center_point O1 O; (BCO) = circle_center_point O2 O; E = intersection (DH1O) (BCO); NO = line N O; AE = line A E; P = intersection NO AE; Prove: concyclic P B O C
Difficulty score: 4.0