Problem (2015CGMOp1): Let $\triangle ABC$ be an acute-angled triangle with $AB>AC$, $O$ be its circumcenter and $D$ the midpoint of side $BC$. The circle with diameter $AD$ meets sides $AB,AC$ again at points $E,F$ respectively. The line passing through $D$ parallel to $AO$ meets $EF$ at $M$. Show that $EM=MF$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = midpoint b c; o1 = midpoint a d; e = on_line a b, on_circle o1 a; f = on_line a c, on_circle o1 a; m = on_line e f, on_pline d a o ? cong e m m f
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; D = midpoint B C; (AD) = circle_diameter A D; AB = line A B; E = intersection (AD) AB; AC = line A C; F = intersection (AD) AC; AO = line A O; l1 = parallel_line D AO; EF = line E F; M = intersection l1 EF; Prove: cong E M M F
Difficulty score: 1.8