Problem (2017IranGOMp2): Two circles $\omega_1,\omega_2$ intersect at $A,B$. An arbitrary line through $B$ meets $\omega_1,\omega_2$ at $C,D$ respectively. The points $E,F$ are chosen on $\omega_1,\omega_2$ respectively so that $CE=CB,\ BD=DF$. Suppose that $BF$ meets $\omega_1$ at $P$, and $BE$ meets $\omega_2$ at $Q$. Prove that $A,P,Q$ are collinear.
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; t = free; c = on_line b t, on_circle o1 a; d = on_line b t, on_circle o2 a; e = on_circle o1 a, on_circle c b; f = on_circle o2 a, on_circle d b; p = on_line b f, on_circle o1 a; q = on_line b e, on_circle o2 a ? coll a p q
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; T = point; BT = line B T; C = intersection BT (O1); D = intersection BT (O2); (C) = circle_center_point C B; E = intersection (O1) (C); (D) = circle_center_point D B; F = intersection (O2) (D); BF = line B F; P = intersection BF (O1); BE = line B E; Q = intersection BE (O2); Prove: collinear A P Q
Difficulty score: 2.1