Problem (2018CTSTp21): In isosceles $\triangle ABC$, $AB=AC$, points $D,E,F$ lie on segments $BC,AC,AB$ such that $DE\parallel AB$, $DF\parallel AC$. The circumcircle of $\triangle ABC$ $\omega_1$ and the circumcircle of $\triangle AEF$ $\omega_2$ intersect at $A,G$. Let $DE$ meet $\omega_2$ at $K\neq E$. Points $L,M$ lie on $\omega_1,\omega_2$ respectively such that $LG\perp KG, MG\perp CG$. Let $P,Q$ be the circumcenters of $\triangle DGL$ and $\triangle DGM$ respectively. Prove that $A,G,P,Q$ are concyclic.
AlphaGeometry formalization: a b c = iso_triangle; d = on_line b c; e = on_line a c, on_pline d a b; f = on_line a b, on_pline d a c; o1 = circumcenter a b c; o2 = circumcenter a e f; g = on_circle o1 a, on_circle o2 a; k = on_line d e, on_circle o2 a; l = on_circle o1 a, on_tline g k g; m = on_circle o2 a, on_tline g c g; p = circumcenter d g l; q = circumcenter d g m ? cyclic a g p q
HAGeo formalization: A B C = isos_triangle; BC = line B C; D = on_line BC; AC = line A C; AB = line A B; l1 = parallel_line D AB; E = intersection AC l1; l2 = parallel_line D AC; F = intersection AB l2; O1 = circumcenter A B C; O2 = circumcenter A E F; (O1) = circle_center_point O1 A; (O2) = circle_center_point O2 A; G = intersection (O1) (O2); DE = line D E; K = intersection DE (O2); KG = line K G; l3 = perpendicular_line G KG; L = intersection (O1) l3; CG = line C G; l4 = perpendicular_line G CG; M = intersection (O2) l4; P = circumcenter D G L; Q = circumcenter D G M; Prove: concyclic A G P Q
Difficulty score: 4.2