Problem (2014IranGOAp4): A tangent line to circumcircle of acute triangle $ABC$ ($AC>AB$) at $A$ intersects with the extension of $BC$ at $P$. $O$ is the circumcenter of triangle $ABC$.Point $X$ lying on $OP$ such that $\measuredangle AXP=90^\circ$.Points $E$ and $F$ lying on $AB$ and $AC$,respectively,and they are in one side of line $OP$ such that $ \measuredangle EXP=\measuredangle ACX $ and $\measuredangle FXO=\measuredangle ABX $. $K$,$L$ are points of intersection $EF$ with circumcircle of triangle $ABC$.prove that $OP$ is tangent to circumcircle of triangle $KLX$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; p = on_tline a o a, on_line b c; x = foot a o p; e = on_line a b, on_aline e x p a c x; f = on_line a c, on_aline f x o a b x; k = on_line e f, on_circle o a; l = on_line e f, on_circle o a; o1 = circumcenter k l x ? perp o x o1 x
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; OA = line O A; ta = perpendicular_line A OA; BC = line B C; P = intersection ta BC; OP = line O P; X = foot A OP; AB = line A B; AC = line A C; l1 = angle_equal1 X P A C X; E = intersection l1 AB; l2 = angle_equal1 X O A B X; F = intersection l2 AC; EF = line E F; (ABC) = circle_center_point O A; K L = intersection EF (ABC); O1 = circumcenter K L X; O1X = line O1 X; Prove: perpendicular O1X OP
Difficulty score: 3.7