Problem (2016CzechAPSlovakp6): Let $ABC$ be an acute-angled triangle with $AB < AC$. Tangent to its circumcircle $\Omega$ at $A$ intersects the line $BC$ at $D$. Let $G$ be the centroid of $\triangle ABC$ and let $AG$ meet $\Omega$ again at $H \neq A$. Suppose the line $DG$ intersects the lines $AB$ and $AC$ at $E$ and $F$, respectively. Prove that $\angle EHG = \angle GHF$
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_line b c, on_tline a o a; x y z g = centroid a b c; h = on_line a g, on_circle o a; e = on_line a b, on_line d g; f = on_line a c, on_line d g ? eqangle e h h g g h h f
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; BC = line B C; OA = line O A; l = perpendicular_line A OA; D = intersection l BC; G X Y Z = centroid A B C; AG = line A G; (O) = circle_center_point O A; H = intersection AG (O); DG = line D G; AB = line A B; E = intersection DG AB; AC = line A C; F = intersection DG AC; Prove: equal_angle E H G G H F
Difficulty score: 3.6