Problem (2019G2): Let $ABC$ be an acute-angled triangle and let $D, E$, and $F$ be the feet of altitudes from $A, B$, and $C$ to sides $BC, CA$, and $AB$, respectively. Denote by $\omega_B$ and $\omega_C$ the incircles of triangles $BDF$ and $CDE$, and let these circles be tangent to segments $DF$ and $DE$ at $M$ and $N$, respectively. Let line $MN$ meet circles $\omega_B$ and $\omega_C$ again at $P \ne M$ and $Q \ne N$, respectively. Prove that $MP = NQ$.
AlphaGeometry formalization: a b c = triangle; d = foot a b c; e = foot b a c; f = foot c a b; i1 = incenter b d f; m = foot i1 d f; i2 = incenter c d e; n = foot i2 d e; p = on_line m n, on_circle i1 m; q = on_line m n, on_circle i2 n ? cong m p n q
HAGeo formalization: A B C = acute_triangle; BC = line B C; D = foot A BC; AC = line A C; E = foot B AC; AB = line A B; F = foot C AB; DF = line D F; I1 = incenter B D F; M = foot I1 DF; I2 = incenter C D E; DE = line D E; N = foot I2 DE; MN = line M N; (I1) = circle_center_point I1 M; P = intersection MN (I1); (I2) = circle_center_point I2 N; Q = intersection MN (I2); Prove: cong M P N Q
Difficulty score: 2.1