Problem (2023IranGOAp1): We are given an acute triangle $ABC$. The angle bisector of $\angle BAC$ cuts $BC$ at $P$. Points $D$ and $E$ lie on segments $AB$ and $AC$, respectively, so that $BC \parallel  DE$. Points $K$ and $L$ lie on segments $PD$ and $PE$, respectively, so that points $A$, $D$, $E$, $K$, $L$ are concyclic. Prove that points $B$, $C$, $K$, $L$ are also concyclic.
AlphaGeometry formalization: a b c = triangle; p = on_line b c, angle_bisector b a c; d = on_line a b; e = on_line a c, on_pline d b c; o1 = circumcenter a d e; k = on_line p d, on_circle o1 a; l = on_line p e, on_circle o1 a ? cyclic b c k l
HAGeo formalization: A B C = acute_triangle; l1 = angle_bisector B A C; BC = line B C; P = intersection l1 BC; AB = line A B; D = on_line AB; l2 = parallel_line D BC; AC = line A C; E = intersection AC l2; DP = line D P; (ADE) = circle A D E; K = intersection DP (ADE); EP = line E P; L = intersection EP (ADE); Prove: concyclic B C K L
Difficulty score: 2.2