Problem (2017RMMSLG1): Let $ABCD$ be a trapezium, $AD\parallel BC$, and let $E,F$ be points on the sides$AB$ and $CD$, respectively. The circumcircle of $AEF$ meets $AD$ again at $A_1$, and the circumcircle of $CEF$ meets $BC$ again at $C_1$. Prove that $A_1C_1,BD,EF$ are concurrent.
AlphaGeometry formalization: d a b c = trapezoid; e = on_line a b; f = on_line c d; a1 = on_line a d, on_circum a e f; c1 = on_line b c, on_circum c e f; x = on_line a1 c1, on_line b d ? coll x e f
HAGeo formalization: A B C D = trapezoid; AB = line A B; E = on_line AB; CD = line C D; F = on_line CD; AD = line A D; (AEF) = circle A E F; A1 = intersection AD (AEF); BC = line B C; (CEF) = circle C E F; C1 = intersection BC (CEF); A1C1 = line A1 C1; BD = line B D; X = intersection A1C1 BD; Prove: collinear X E F
Difficulty score: 3.1