Problem (2018IranGOAp1): Two circles $\omega_1,\omega_2$ intersect each other at points $A,B$. Let $PQ$ be a common tangent line of these two circles with $P \in \omega_1$ and $Q  \in  \omega_2$. An arbitrary point $X$ lies on $\omega_1$. Line $AX$ intersects $ \omega_2$ for the second time at $Y$ . Point $Y'\ne Y$ lies on $\omega_2$ such that $QY = QY'$. Line $Y'B$ intersects $ \omega_1$ for the second time at $X'$. Prove that $PX = PX'$.
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; p q p1 q1 = cc_tangent p q p1 q1 o1 a o2 a; x = on_circle o1 a; y = on_line a x, on_circle o2 a; y1 = on_circle o2 a, on_circle q y; x1 = on_line y1 b, on_circle o1 a ? cong p x p x1
HAGeo formalization: A = point; B = point; l = perpendicular_bisector A B; O1 = on_line l; O2 = on_line l; (O1) = circle_center_point O1 A; (O2) = circle_center_point O2 A; l1 = ex_common_tangent (O1) (O2); P = intersection l1 (O1); Q = intersection l1 (O2); X = on_circle (O1); AX = line A X; Y = intersection AX (O2); (Q) = circle_center_point Q Y; Y1 = intersection (O2) (Q); BY1 = line B Y1; X1 = intersection BY1 (O1); Prove: cong P X P X1
Difficulty score: 1.9