Problem (2020AQGOp5): Let $\Delta ABC$ be a triangle and let the incircle meet $\overline{BC},\overline{CA},\overline{AB}$ at $D,E,F$ respectively . Let $\overline{DI}$ intersect $(ABC)$ at points $X,Y$ such that $X,I,D,Y$ are in this order. Let $(XFE)$ intersect $(ABC)$ at $T$ and $(DXT)$ intersect the incircle at $K$. Let $\overline{AX}$ intersect $\overline{BC}$ at $M$ and $\overline{AY}$ intersect $\overline{BC}$ at $N$ and let $(AMN)$ intersect $(ABC)$ at $R$. Then prove that $A,K,R$ are collinear.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; e = foot i a c; f = foot i a b; o = circumcenter a b c; x = on_line d i, on_circle o a; y = on_line d i, on_circle o a; o1 = circumcenter x f e; t = on_circle o1 x, on_circle o a; o2 = circumcenter d x t; k = on_circle o2 d, on_circle i d; m = on_line a x, on_line b c; n = on_line a y, on_line b c; o3 = circumcenter a m n; r = on_circle o3 a, on_circle o a ? coll a k r
HAGeo formalization: A B C = triangle; I = incenter A B C; I = incenter A B C; BC = line B C; D = foot I BC; (I) = circle_center_point I D; AC = line A C; E = foot I AC; AB = line A B; F = foot I AB; DI = line D I; O = circumcenter A B C; (ABC) = circle_center_point O A; X = intersection DI (ABC); Y = intersection DI (ABC); O1 = circumcenter E F X; (EFX) = circle_center_point O1 X; T = intersection (EFX) (ABC); O2 = circumcenter D T X; (DTX) = circle_center_point O2 D; K = intersection (DTX) (I); AX = line A X; M = intersection AX BC; AY = line A Y; N = intersection AY BC; O3 = circumcenter A M N; (AMN) = circle_center_point O3 A; R = intersection (AMN) (ABC); Prove: collinear A K R
Difficulty score: 5.2