Problem (2024ShuZhiMiMOM12p2): In $\triangle ABC$, let $X$ be a point distinct from the orthocenter. Lines $AX$, $BX$, $CX$ meet the circumcircle at $X_A$, $X_B$, $X_C$. Let $Y$ be the isogonal conjugate of $X$ in $\triangle X_AX_BX_C$. Lines $AX$ and $YX$ meet the circumcircle of $\triangle BXC$ at $P$ and $Q$ (other than $X$). Line $PQ$ meets $BC$ at $R$. Prove $PR = AR$.
AlphaGeometry formalization: a b c = triangle; x = free; o = circumcenter a b c; x1 = on_line a x, on_circle o a; x2 = on_line b x, on_circle o a; x3 = on_line c x, on_circle o a; y = on_aline y x1 x2 x3 x1 x, on_aline y x2 x1 x3 x2 x; o1 = circumcenter b x c; p = on_line a x, on_circle o1 b; q = on_line y x, on_circle o1 b; r = on_line p q, on_line b c ? cong p r a r
HAGeo formalization: A B C = triangle; X = point; O = circumcenter A B C; AX = line A X; (O) = circle_center_point O A; X1 = intersection AX (O); BX = line B X; X2 = intersection BX (O); CX = line C X; X3 = intersection CX (O); l1 = angle_equal1 X1 X2 X3 X1 X; l2 = angle_equal1 X2 X1 X3 X2 X; Y = intersection l1 l2; O1 = circumcenter B X C; (O1) = circle_center_point O1 B; P = intersection AX (O1); YX = line Y X; Q = intersection YX (O1); PQ = line P Q; BC = line B C; R = intersection PQ BC; Prove: cong P R A R
Difficulty score: 5.0