Problem (2017IOMetrop1): Let $ABCD$ be a parallelogram in which angle at $B$ is obtuse and $AD>AB$. Points $K$ and $L$ on $AC$ such that $\angle ADL=\angle KBA$(the points $A, K, C, L$ are all different, with $K$ between $A$ and $L$). The line $BK$ intersects the circumcircle $\omega$ of $ABC$ at points $B$ and $E$, and the line $EL$ intersects $\omega$ at points $E$ and $F$. Prove that $BF||AC$.
AlphaGeometry formalization: a b c = triangle; d = parallelogram a b c d; k = on_line a c; l = on_line a c, on_aline l d a a b k; o = circumcenter a b c; e = on_line b k, on_circle o a; f = on_line e l, on_circle o a ? para b f a c
HAGeo formalization: A B C D = parallelogram; AC = line A C; K = on_line AC; l = angle_equal1 D A A B K; L = intersection AC l; BK = line B K; O = circumcenter A B C; (O) = circle_center_point O A; E = intersection BK (O); EL = line E L; F = intersection EL (O); BF = line B F; Prove: parallel BF AC
Difficulty score: 2.0