Problem (2009CGMOp2): Right triangle $ ABC,$ with $ \angle A=90^{\circ},$ is inscribed in circle $ \Gamma.$ Point $ E$ lies on the interior of arc $ {BC}$ (not containing $ A$) with $ EA>EC.$ Point $ F$ lies on ray $ EC$ with $ \angle EAC = \angle CAF.$ Segment $ BF$ meets $ \Gamma$ again at $ D$ (other than $ B$). Let $ O$ denote the circumcenter of triangle $ DEF.$ Prove that $ A,C,O$ are collinear.
AlphaGeometry formalization: a b c = r_triangle; o = midpoint b c; e = on_circle o a; f = on_line c e, on_aline f a c c a e; d = on_line b f, on_circle o a; o1 = circumcenter d e f ? coll a c o1
HAGeo formalization: A B C = right_triangle; O = midpoint B C; (O) = circle_center_point O A; E = on_circle (O); CE = line C E; l = angle_equal1 A C C A E; F = intersection CE l; BF = line B F; D = intersection BF (O); O1 = circumcenter D E F; Prove: collinear A C O1
Difficulty score: 1.7