Problem (2019CHNNorthernMOp5): Two circles $O_1$ and $O_2$ intersect at $A,B$. Bisector of outer angle $\angle O_1AO_2$ intersects $O_1$ at $C$, $O_2$ at $D$. $P$ is a point on $\odot(BCD)$, $CP\cap O_1=E,DP\cap O_2=F$. Prove that $PE=PF$.
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; c = on_circle o1 a, angle_bisector o1 a o2; d = on_circle o2 a, angle_bisector o1 a o2; o3 = circumcenter b c d; p = on_circle o3 b; e = on_line c p, on_circle o1 a; f = on_line d p, on_circle o2 a ? cong p e p f
HAGeo formalization: (O1) = circle; (O2) = circle; O1 = circumcenter (O1); O2 = circumcenter (O2); A B = intersection (O1) (O2); l = angle_bisector O1 A O2; C = intersection l (O1); D = intersection l (O2); (BCD) = circle B C D; P = on_circle (BCD); CP = line C P; E = intersection CP (O1); DP = line D P; F = intersection DP (O2); EP = line E P; FP = line F P; Prove: cong E P F P
Difficulty score: 1.6