Problem (2020EuropeanMCupSp1): Let $ABCD$ be a parallelogram such that $|AB| > |BC|$. Let $O$ be a point on the line $CD$ such that $|OB| = |OD|$. Let $\omega$ be a circle with center $O$ and radius $|OC|$. If $T$ is the second intersection of $\omega$ and $CD$, prove that $AT, BO$ and $\omega$ are concurrent.
AlphaGeometry formalization: a b c = triangle; d = parallelogram a b c d; o = on_line c d, on_bline b d; t = on_line c d, on_circle o c; x = on_line a t, on_line o b ? cong o x o c
HAGeo formalization: A B C D = parallelogram; l1 = perpendicular_bisector B D; CD = line C D; O = intersection CD l1; (O) = circle_center_point O C; T = intersection CD (O); AT = line A T; BO = line B O; X = intersection AT BO; Prove: cong O X O C
Difficulty score: 1.4