Problem (2021IranGOAp1): Acute-angled triangle $ABC$ with circumcircle $\omega$ is given. Let $D$ be the midpoint of $AC$, $E$ be the foot of altitude from $A$ to $BC$, and $F$ be the intersection point of $AB$ and $DE$. Point $H$ lies on the arc $BC$ of $\omega$ (the one that does not contain $A$) such that $\angle BHE=\angle ABC$. Prove that $\angle BHF=90^\circ$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = midpoint a c; e = foot a b c; f = on_line a b, on_line d e; h = on_circle o a, eqangle3 h b e b a c ? perp b h h f
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; (O) = circle_center_point O A; D = midpoint A C; BC = line B C; E = foot A BC; AB = line A B; DE = line D E; F = intersection AB DE; ω1 = angle_equal2 B E A B C; H = intersection (O) ω1; BH = line B H; HF = line H F; Prove: perpendicular BH HF
Difficulty score: 2.0