Problem (2009G4): Given a cyclic quadrilateral $ABCD$, let the diagonals $AC$ and $BD$ meet at $E$ and the lines $AD$ and $BC$ meet at $F$. The midpoints of $AB$ and $CD$ are $G$ and $H$, respectively. Show that $EF$ is tangent at $E$ to the circle through the points $E$, $G$ and $H$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_circle o a; e = on_line a c, on_line b d; f = on_line a d, on_line b c; g = midpoint a b; h = midpoint c d; o1 = circumcenter e g h ? perp o1 e e f
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (O) = circle_center_point O A; D = on_circle (O); AC = line A C; BD = line B D; E = intersection AC BD; AD = line A D; BC = line B C; F = intersection AD BC; G = midpoint A B; H = midpoint C D; EF = line E F; O1 = circumcenter E G H; O1E = line O1 E; Prove: perpendicular O1E EF
Difficulty score: 2.8