Problem (2007CHNSouthEastMOp2): $AB$ is the diameter of semicircle $O$. $C$,$D$ are two arbitrary points on semicircle $O$. Point $P$ lies on line $CD$ such that line $PB$ is tangent to semicircle $O$ at $B$. Line $PO$ intersects line $CA$, $AD$ at point $E$, $F$ respectively. Prove that $OE$=$OF$.
AlphaGeometry formalization: a b = segment; o = midpoint a b; c = on_circle o a; d = on_circle o a; p = on_line c d, on_tline b o b; e = on_line c a, on_line p o; f = on_line a d, on_line p o ? cong o e o f
HAGeo formalization: A = point; B = point; O = midpoint A B; (O) = circle_center_point O A; C = on_circle (O); D = on_circle (O); OB = line O B; l1 = perpendicular_line B OB; CD = line C D; P = intersection CD l1; OP = line O P; AC = line A C; E = intersection OP AC; AD = line A D; F = intersection OP AD; Prove: cong E O F O
Difficulty score: 2.8