Problem (2012ARMOg10p2): The inscribed circle $\omega$ of the non-isosceles acute-angled triangle $ABC$ touches the side $BC$ at the point $D$. Suppose that $I$ and $O$ are the centres of inscribed circle and circumcircle of triangle $ABC$ respectively. The circumcircle of triangle $ADI$ intersects $AO$ at the points $A$ and $E$. Prove that $AE$ is equal to the radius $r$ of $\omega$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; o = circumcenter a b c; e = on_line a o, on_circum a d i ? cong a e i d
HAGeo formalization: A B C = acute_triangle; I = incenter A B C; BC = line B C; D = foot I BC; O = circumcenter A B C; AO = line A O; (ADI) = circle A D I; E = intersection AO (ADI); AE = line A E; DI = line D I; Prove: cong A E D I
Difficulty score: 1.9