Problem (2016IranGOMp2): Let two circles $C_1$ and $C_2$ intersect in points $A$ and $B$. The tangent to $C_1$ at $A$ intersects $C_2$ in $P$ and the line $PB$ intersects $C_1$ for the second time in $Q$ (suppose that $Q$ is outside $C_2$). The tangent to $C_2$ from $Q$ intersects $C_1$ and $C_2$ in $C$ and $D$, respectively. (The points $A$ and $D$ lie on different sides of the line $PQ$.) Show that $AD$ is the bisector of $\angle CAP$.
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; p = on_tline a o1 a, on_circle o2 a; q = on_line p b, on_circle o1 a; d1 d2 = tangent q o2 a; c = on_line q d1, on_circle o1 a ? eqangle c a a d1 d1 a a p
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 = tangent_line A (O1); P = intersection l1 (O2); BP = line B P; Q = intersection BP (O1); l2 = tangent_line Q (O2); C = intersection l2 (O1); D = intersection l2 (O2); Prove: equal_angle C A D D A P
Difficulty score: 1.5