Problem (2012CHNSouthEastMOp2): The incircle $I$ of $\triangle ABC$ is tangent to sides $AB,BC,CA$ at $D,E,F$ respectively. Line $EF$ intersects lines $AI,BI,DI$ at $M,N,K$ respectively. Prove that $DM\cdot KE=DN\cdot KF$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i a b; e = foot i b c; f = foot i a c; m = on_line e f, on_line a i; n = on_line e f, on_line b i; k = on_line e f, on_line d i ? eqratio d m d n k f k e
HAGeo formalization: A B C = triangle; I = incenter A B C; AB = line A B; D = foot I AB; BC = line B C; E = foot I BC; AC = line A C; F = foot I AC; EF = line E F; AI = line A I; M = intersection EF AI; BI = line B I; N = intersection EF BI; DI = line D I; K = intersection EF DI; Prove: equal_ratio D M D N F K E K
Difficulty score: 2.1