Problem (2014CHNGaoLian): Let $ABC$ be an acute triangle such that $\angle BAC \neq 60^\circ$. Let $D,E$ be points such that $BD,CE$ are tangent to the circumcircle of $ABC$ and $BD=CE=BC$ ($A$ is on one side of line $BC$ and $D,E$ are on the other side). Let $F,G$ be intersections of line $DE$ and lines $AB,AC$. Let $M$ be intersection of $CF$ and $BD$, and $N$ be intersection of $CE$ and $BG$. Prove that $AM=AN$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_tline b o b, on_circle b c; e = on_tline c o c, on_circle c b; f = on_line a b, on_line d e; g = on_line a c, on_line d e; m = on_line c f, on_line b d; n = on_line c e, on_line b g ? cong a m a n
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; OB = line O B; l1 = perpendicular_line B OB; (B) = circle_center_point B C; D = intersection l1 (B); OC = line O C; l2 = perpendicular_line C OC; (C) = circle_center_point C B; E = intersection l2 (C); DE = line D E; AB = line A B; F = intersection DE AB; AC = line A C; G = intersection DE AC; CF = line C F; BD = line B D; M = intersection CF BD; CE = line C E; BG = line B G; N = intersection CE BG; AM = line A M; AN = line A N; Prove: cong A M A N
Difficulty score: 2.8