Problem (2009CTSTp19): Let $ ABC$ be a triangle. Point $ D$ lies on its sideline $ BC$ such that $ \angle CAD = \angle CBA.$ Circle $ (O)$ passing through $ B,D$ intersects $ AB,AD$ at $ E,F$, respectively. $ BF$ meets $ DE$ at $ G$.Denote by$ M$ the midpoint of $ AG.$ Show that $ CM\perp AO.$
AlphaGeometry formalization: a b c = triangle; d = on_line b c, on_aline d a c c b a; e = on_line a b; o = circumcenter b d e; f = on_line a d, on_circle o b; g = on_line b f, on_line d e; m = midpoint a g ? perp c m a o
HAGeo formalization: A B C = triangle; BC = line B C; l1 = angle_equal1 A C C B A; D = intersection BC l1; AB = line A B; E = on_line AB; O = circumcenter B D E; (O) = circle_center_point O B; AD = line A D; F = intersection AD (O); BF = line B F; DE = line D E; G = intersection BF DE; M = midpoint A G; CM = line C M; AO = line A O; Prove: perpendicular CM AO
Difficulty score: 2.7