Problem (2017CzechAPSlovakp2): Let ${\omega}$ be the circumcircle of an acute-angled triangle ${ABC}$. Point ${D}$ lies on the arc ${BC}$ of ${\omega}$ not containing point ${A}$. Point ${E}$ lies in the interior of the triangle ${ABC}$, does not lie on the line ${AD}$, and satisfies ${\angle DBE =\angle ACB}$ and ${\angle DCE = \angle ABC}$. Let ${F}$ be a point on the line ${AD}$ such that lines ${EF}$ and ${BC}$ are parallel, and let ${G}$ be a point on ${\omega}$ different from ${A}$ such that ${AF = FG}$. Prove that points ${D,E, F,G}$ lie on one circle.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; e = on_aline e b d b c a, on_aline e c d c b a; f = on_line a d, on_pline e b c; g = on_circle f a, on_circum a b c ? cyclic d e f g
HAGeo formalization: A B C = acute_triangle; (ABC) = circumcircle A B C; D = on_circle (ABC); l1 = angle_equal1 B D B C A; l2 = angle_equal1 C D C B A; E = intersection l1 l2; BC = line B C; l3 = parallel_line E BC; AD = line A D; F = intersection AD l3; (F) = circle_center_point F A; G = intersection (ABC) (F); Prove: concyclic D E F G
Difficulty score: 3.3