Problem (2020BalkanMOp1): Let $ABC$ be an acute triangle with $AB=AC$, let $D$ be the midpoint of the side $AC$, and let $\gamma$ be the circumcircle of the triangle $ABD$. The tangent of $\gamma$ at $A$ crosses the line $BC$ at $E$. Let $O$ be the circumcenter of the triangle $ABE$. Prove that midpoint of the segment $AO$ lies on $\gamma$.
AlphaGeometry formalization: a b c = iso_triangle; d = midpoint a c; o1 = circumcenter a b d; e = on_line b c, on_tline a o1 a; o = circumcenter a b e; m = midpoint a o ? cong o1 a o1 m
HAGeo formalization: A B C = isos_triangle; D = midpoint A C; O1 = circumcenter A B D; O1A = line O1 A; l1 = perpendicular_line A O1A; BC = line B C; E = intersection l1 BC; O = circumcenter A B E; M = midpoint A O; Prove: cong O1 A O1 M
Difficulty score: 2.1