Problem (2023IranGOMp4): Let $ABC$ be a triangle and $P$ be the midpoint of arc $BAC$ of circumcircle of triangle $ABC$ with orthocenter $H$. Let $Q, S$ be points such that $HAPQ$ and $SACQ$ are parallelograms. Let $T$ be the midpoint of $AQ$, and $R$ be the intersection point of the lines $SQ$ and $PB$. Prove that $AB$, $SH$ and $TR$ are concurrent.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; o = circumcenter a b c; p = on_bline b c, on_circle o a; q = parallelogram h a p q; s = parallelogram a c q s; t = midpoint a q; r = on_line s q, on_line p b; x = on_line a b, on_line s h ? coll x t r
HAGeo formalization: A B C = triangle; H = orthocenter A B C; O = circumcenter A B C; P = midarc_no B C A; Q = parallelogram H A P; S = parallelogram A C Q; T = midpoint A Q; QS = line Q S; BP = line B P; R = intersection QS BP; AB = line A B; HS = line H S; X = intersection AB HS; Prove: collinear X T R
Difficulty score: 4.2