Problem (2021ARMOg10p1): On the side $BC$ of the parallelogram $ABCD$, points $E$ and $F$ are given ($E$ lies between $B$ and $F$) and the diagonals $AC, BD$ meet at $O$. If it's known that $AE, DF$ are tangent to the circumcircle of $\triangle AOD$, prove that they're tangent to the circumcircle of $\triangle EOF$ as well.
AlphaGeometry formalization: a b c = triangle; d = parallelogram a b c d; o = on_line a c, on_line b d; o1 = circumcenter a o d; e = on_line b c, on_tline a o1 a; f = on_line b c, on_tline d o1 d; o2 = circumcenter e o f ? perp o2 e a e
HAGeo formalization: A B C D = parallelogram; AC = line A C; BD = line B D; O = intersection AC BD; (ADO) = circle A D O; l1 = tangent A (ADO); BC = line B C; E = intersection BC l1; l2 = tangent D (ADO); F = intersection BC l2; AE = line A E; O2 = circumcenter E F O; EO2 = line E O2; Prove: perpendicular AE EO2
Difficulty score: 1.9