Problem (2017IranTSTp18): In triangle $ABC$ let $O$ and $H$ be the circumcenter and the orthocenter. The point $P$ is the reflection of $A$ with respect to $OH$. Assume that $P$ is not on the same side of $BC$ as $A$. Points $E,F$ lie on $AB,AC$ respectively such that $BE=PC \ ,  CF=PB$. Let $K$ be the intersection point of $AP,OH$. Prove that $\angle EKF = 90 ^{\circ}$
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; p = reflect a o h; e = on_line a b, eqdistance e b p c; f = on_line a c, eqdistance f c p b; k = on_line a p, on_line o h ? perp e k f k
HAGeo formalization: A B C = triangle; O = circumcenter A B C; H = orthocenter A B C; OH  = line O H; P = reflect_point_wrt_line A OH; AB = line A B; (B) = circle_center_radius B P C; E = intersection AB (B); AC = line A C; (C) = circle_center_radius C P B; F = intersection AC (C); AP = line A P; OH = line O H; K = intersection AP OH; EK = line E K; FK = line F K; Prove: perpendicular EK FK
Difficulty score: 4.5