Problem (2019ARMOg9p3): Circle $\Omega$ with center $O$ is the circumcircle of an acute triangle $\triangle ABC$ with $AB<BC$ and orthocenter $H$. On the line $BO$ there is point $D$ such that $O$ is between $B$ and $D$ and $\angle ADC= \angle ABC$ . The semi-line starting at $H$ and parallel to $BO$ wich intersects segment $AC$ , intersects $\Omega$ at $E$. Prove that $BH=DE$.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; o = circumcenter a b c; d = on_line b o, eqangle3 d a c b c a; e = on_circle o a, on_pline h b o ? cong b h d e
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; (O) = circle_center_point O A; H = orthocenter A B C; BO = line B O; ω1 = angle_equal2 A C C B A; D = intersection BO ω1; l2 = parallel_line H BO; E = intersection l2 (O); Prove: cong B H D E
Difficulty score: 3.2