Problem (20**_11thXueErSiMO): Let $\triangle ABC$ have circumcircle $\Gamma$. The angle bisector of $\angle BAC$ intersects $BC$ at $D$. Point $P$ lies on segment $AD$. Straight line $BP$ intersects $AC$ at $E$, and straight line $CP$ intersects $AB$ at $F$. Let the tangent of the circle $\Gamma$ at point $A$ intersect the line $EF$ at the point $Q$. Prove that $PQ\parallel BC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_line b c, angle_bisector b a c; p = on_line a d; e = on_line b p, on_line a c; f = on_line c p, on_line a b; q = on_line e f, on_tline a o a ? para p q b c
HAGeo formalization: A B C = triangle; O = circumcenter A B C; l1 = angle_bisector B A C; BC = line B C; D = intersection l1 BC; AD = line A D; P = on_line AD; BP = line B P; AC = line A C; E = intersection BP AC; CP = line C P; AB = line A B; F = intersection CP AB; OA = line O A; l = perpendicular_line A OA; EF = line E F; Q = intersection l EF; PQ = line P Q; Prove: parallel PQ BC
Difficulty score: 2.5