Problem (2010CHNWesternMOp6): $\Delta ABC$ is a right-angled triangle, $\angle C = 90^{\circ}$. Draw a circle centered at $B$ with radius $BC$. Let $D$ be a point on the side $AC$, and $DE$ is tangent to the circle at $E$. The line through $C$ perpendicular to $AB$ meets line $BE$ at $F$. Line $AF$ meets $DE$ at point $G$. The line through $A$ parallel to $BG$ meets $DE$ at $H$. Prove that $GE = GH$.
AlphaGeometry formalization: c a b = r_triangle; e = on_circle b c; d = on_line a c, on_tline e b e; f = on_line b e, on_tline c a b; g = on_line a f, on_line d e; h = on_line d e, on_pline a b g ? midp g e h
HAGeo formalization: C A B = right_triangle; (B) = circle_center_point B C; E = on_circle (B); AC = line A C; BE = line B E; l1 = perpendicular_line E BE; D = intersection AC l1; AB = line A B; l2 = perpendicular_line C AB; BE = line B E; F = intersection l2 BE; AF = line A F; DE = line D E; G = intersection AF DE; BG = line B G; l3 = parallel_line A BG; H = intersection l3 DE; Prove: midpoint G E H
Difficulty score: 2.8