Problem (2014BulgariaMOp6): Let $ABCD$ be a quadrilateral inscribed in a circle $k$. $AC$ and $BD$ meet at $E$. The rays $\overrightarrow{CB}, \overrightarrow{DA}$ meet at $F$. Prove that the line through the incenters of $\triangle ABE\,,\, \triangle ABF$ and the line through the incenters of $\triangle CDE\,,\, \triangle CDF$ meet at a point lying on the circle $k$.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; o = circumcenter a b c; e = on_line a c, on_line b d; f = on_line c b, on_line d a; i1 = incenter a b e; i2 = incenter a b f; i3 = incenter c d e; i4 = incenter c d f; p = on_line i1 i2, on_line i3 i4 ? cyclic p a b c
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); O = circumcenter A B C; AC = line A C; BD = line B D; E = intersection AC BD; CB = line C B; DA = line D A; F = intersection CB DA; I1 = incenter A B E; I2 = incenter A B F; I3 = incenter C D E; I4 = incenter C D F; I1I2 = line I1 I2; I3I4 = line I3 I4; P = intersection I1I2 I3I4; Prove: concyclic P A B C
Difficulty score: 4.6