Problem (2005CHNWesternMOp2): Given three points $P$, $A$, $B$ and a circle such that the lines $PA$ and $PB$ are tangent to the circle at the points $A$ and $B$, respectively. A line through the point $P$ intersects that circle at two points $C$ and $D$. Through the point $B$, draw a line parallel to $PA$; let this line intersect the lines $AC$ and $AD$ at the points $E$ and $F$, respectively. Prove that $BE = BF$.
AlphaGeometry formalization: o a b = iso_triangle; p = on_tline a o a, on_tline b o b; t = free; c = on_circle o a; d = on_line p c, on_circle o a; e = on_line a c, on_pline b p a; f = on_line a d, on_pline b p a ? cong b e b f
HAGeo formalization: O A B = isos_triangle; OA = line O A; OB = line O B; l1 = perpendicular_line A OA; l2 = perpendicular_line B OB; P = intersection l1 l2; (O) = circle_center_point O A; C = on_circle (O); CP = line C P; D = intersection CP (O); AP = line A P; l3 = parallel_line B AP; AC = line A C; E = intersection l3 AC; AD = line A D; F = intersection l3 AD; Prove: cong B E B F
Difficulty score: 1.7