Problem (2016IranGOAp1): Let the circles $\omega$ and $\omega^ \prime$ intersect in $A$ and $B$. Tangent to circle$\omega$ at $A$ intersects$\omega^ \prime$ in $C$ and tangent to circle $\omega^ \prime$ at $A$ intersects $\omega$ in $D$. Suppose that $CD$ intersects$\omega$ and $\omega^ \prime$ in $E$ and $F$, respectively (assume that $E$ is between $F$ and $C$). The perpendicular to $AC$ from $E$ intersects $\omega^ \prime$ in point $P$ and perpendicular to $AD$ from $F$ intersects$\omega$ in point $Q$ (The points $A, P$ and $Q$ lie on the same side of the line $CD$). Prove that the points $A, P$ and $Q$ are collinear.
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; c = on_circle o2 a, on_tline a o1 a; d = on_circle o1 a, on_tline a o2 a; e = on_line c d, on_circle o1 a; f = on_line c d, on_circle o2 a; p = on_circle o2 a, on_tline e a c; q = on_circle o1 a, on_tline f a d ? 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; O1A = line O1 A; l1 = perpendicular_line A O1A; C = intersection l1 (O2); O2A = line O2 A; l2 = perpendicular_line A O2A; D = intersection l2 (O1); CD = line C D; E = intersection CD (O1); F = intersection CD (O2); AC = line A C; l3 = perpendicular_line E AC; P = intersection l3 (O2); AD = line A D; l4 = perpendicular_line F AD; Q = intersection l4 (O1); Prove: collinear A P Q
Difficulty score: 2.0