Problem (2021EGMOp3): Let $ABC$ be a triangle with an obtuse angle at $A$. Let $E$ and $F$ be the intersections of the external bisector of angle $A$ with the altitudes of $ABC$ through $B$ and $C$ respectively. Let $M$ and $N$ be the points on the segments $EC$ and $FB$ respectively such that $\angle EMA = \angle BCA$ and $\angle ANF = \angle ABC$. Prove that the points $E, F, N, M$ lie on a circle.
AlphaGeometry formalization: a b c = triangle; p = angle_bisector b a c; e = on_tline a a p, on_tline b a c; f = on_tline a a p, on_tline c a b; m = on_line e c, eqangle3 m a e c a b; n = on_line f b, eqangle3 n a f b a c ? cyclic e f n m
HAGeo formalization: A B C = obtuse_triangle; l1 = angle_exbisector B A C; AC = line A C; l2 = perpendicular_line B AC; E = intersection l1 l2; AB = line A B; l3 = perpendicular_line C AB; F = intersection l1 l3; ω1 = angle_equal2 E A B C A; CE = line C E; M = intersection CE ω1; BF = line B F; ω2 = angle_equal2 A F A B C; N = intersection BF ω2; Prove: concyclic E F N M
Difficulty score: 3.9