Problem (2017USATSTSTp5): Let $ABC$ be a triangle with incenter $I$. Let $D$ be a point on side $BC$ and let $\omega_B$ and $\omega_C$ be the incircles of $\triangle ABD$ and $\triangle ACD$, respectively. Suppose that $\omega_B$ and $\omega_C$ are tangent to segment $BC$ at points $E$ and $F$, respectively. Let $P$ be the intersection of segment $AD$ with the line joining the centers of $\omega_B$ and $\omega_C$. Let $X$ be the intersection point of lines $BI$ and $CP$ and let $Y$ be the intersection point of lines $CI$ and $BP$. Prove that lines $EX$ and $FY$ meet on the incircle of $\triangle ABC$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = on_line b c; i2 = incenter a b d; i3 = incenter a c d; e = foot i2 b d; f = foot i3 c d; p = on_line a d, on_line i2 i3; x = on_line b i, on_line c p; y = on_line c i, on_line b p; z = on_line e x, on_line f y; d1 = foot i b c ? cong z i d1 i
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; D = on_line BC; Ib = incenter A B D; Ic = incenter A C D; E = foot Ib BC; F = foot Ic BC; AD = line A D; IbIc = line Ib Ic; P = intersection AD IbIc; BI = line B I; CP = line C P; X = intersection BI CP; CI = line C I; BP = line B P; Y = intersection CI BP; EX = line E X; FY = line F Y; Q = intersection EX FY; D1 = foot I BC; Prove: cong Q I D1 I
Difficulty score: 2.9