Problem (2012AsiaPacificMOp4): Let $ ABC $ be an acute triangle. Denote by $ D $ the foot of the perpendicular line drawn from the point $ A $ to the side $ BC $, by $M$ the midpoint of $ BC $, and by $ H $ the orthocenter of $ ABC $. Let $ E $ be the point of intersection of the circumcircle $ \Gamma $ of the triangle $ ABC $ and the half line $ MH $, and $ F $ be the point of intersection (other than $E$) of the line $ ED $ and the circle $ \Gamma $. Prove that $ \tfrac{BF}{CF} = \tfrac{AB}{AC} $ must hold.
AlphaGeometry formalization: a b c = triangle; d = foot a b c; m = midpoint b c; h = orthocenter a b c; e = on_line m h, on_circum a b c; f = on_line e d, on_circum a b c ? eqratio b f f c a b a c
HAGeo formalization: A B C = acute_triangle; BC = line B C; D = foot A BC; M = midpoint B C; H = orthocenter A B C; HM = line H M; (ABC) = circle A B C; E = intersection HM (ABC); DE = line D E; F = intersection DE (ABC); Prove: equal_ratio B F C F A B A C
Difficulty score: 2.1