Problem (1999USAMOp6): Let $ABCD$ be an isosceles trapezoid with $AB \parallel CD$. The inscribed circle $\omega$ of triangle $BCD$ meets $CD$ at $E$. Let $F$ be a point on the (internal) angle bisector of $\angle DAC$ such that $EF \perp CD$. Let the circumscribed circle of triangle $ACF$ meet line $CD$ at $C$ and $G$. Prove that the triangle $AFG$ is isosceles.
AlphaGeometry formalization: a b c d = eq_trapezoid; i = incenter b c d; e = foot i c d; f = angle_bisector d a c, on_tline e c d; o = circumcenter a c f; g = on_line c d, on_circle o a ? cong a f f g
HAGeo formalization: D A B C = isos_trapezoid; I = incenter B C D; CD = line C D; E = foot I CD; l1 = angle_bisector D A C; l2 = perpendicular_line E CD; F = intersection l1 l2; O1 = circumcenter A C F; (O1) = circle_center_point O1 A; G = intersection (O1) CD; Prove: cong F A F G
Difficulty score: 2.1