Problem (2019CMOp3): Let $O$ be the circumcenter of $\triangle ABC$($AB<AC$), and $D$ be a point on the internal angle bisector of $\angle BAC$. Point $E$ lies on $BC$, satisfying $OE\parallel AD$, $DE\perp BC$. Point $K$ lies on $EB$ extended such that $EK=EA$. The circumcircle of $\triangle ADK$ meets $BC$ at $P\neq K$, and meets the circumcircle of $\triangle ABC$ at $Q\neq A$. Prove that $PQ$ is tangent to the circumcircle of $\triangle ABC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; x = angle_bisector b a c; e = on_line b c, on_pline o a x; d = angle_bisector b a c, on_tline e b c; k = on_line e b, on_circle e a; p = on_line b c, on_circum a d k; q = on_circum a b c, on_circum a d k ? perp o q p q
HAGeo formalization: A B C = triangle; O = circumcenter A B C; l = angle_bisector B A C; l1 = parallel_line O l; BC = line B C; E = intersection BC l1; l3 = perpendicular_line E BC; D = intersection l l3; BE = line B E; (E,A) = circle_center_point E A; K = intersection BE (E,A); (ADK) = circle A D K; P = intersection (ADK) BC; (ABC) = circle A B C; Q = intersection (ADK) (ABC); PQ = line P Q; OQ = line O Q; Prove: perpendicular OQ PQ
Difficulty score: 3.6