Problem (2008CTSTp19): Let $ ABC$ be a triangle, let $ AB > AC$. Its incircle touches side $ BC$ at point $ E$. Point $ D$ is the second intersection of the incircle with segment $ AE$ (different from $ E$). Point $ F$ (different from $ E$) is taken on segment $ AE$ such that $ CE = CF$. The ray $ CF$ meets $ BD$ at point $ G$. Show that $ CF = FG$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; e = foot i b c; d = on_line a e, on_circle i e; f = on_line a e, on_circle c e; g = on_line c f, on_line b d ? cong c f f g
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; E = foot I BC; (I) = circle_center_point I E; AE = line A E; D = intersection AE (I); (C) = circle_center_point C E; F = intersection AE (C); BD = line B D; CF = line C F; G = intersection BD CF; Prove: cong C F F G
Difficulty score: 2.6