Problem (2010CGMOp2): In triangle $ABC$, $AB = AC$. Point $D$ is the midpoint of side $BC$. Point $E$ lies outside the triangle $ABC$ such that $CE \perp AB$ and $BE = BD$. Let $M$ be the midpoint of segment $BE$. Point $F$ lies on the minor arc $\widehat{AD}$ of the circumcircle of triangle $ABD$ such that $MF \perp BE$. Prove that $ED \perp FD.$
AlphaGeometry formalization: a b c = iso_triangle; d = midpoint b c; e = on_tline c a b, on_circle b d; m = midpoint b e; o = circumcenter a b d; f = on_circle o a, on_tline m b e ? perp e d f d
HAGeo formalization: A B C = isos_triangle; D = midpoint B C; AB = line A B; l1 = perpendicular_line C AB; (B,D) = circle_center_point B D; E = intersection l1 (B,D); M = midpoint B E; BE = line B E; l2 = perpendicular_line M BE; O1 = circumcenter A B D; (ABD) = circle_center_point O1 A; F = intersection (ABD) l2; DE = line D E; DF = line D F; Prove: perpendicular DE DF
Difficulty score: 3.1