Problem (2012G3): In an acute triangle $ABC$ the points $D,E$ and $F$ are the feet of the altitudes through $A,B$ and $C$ respectively. The incenters of the triangles $AEF$ and $BDF$ are $I_1$ and $I_2$ respectively; the circumcenters of the triangles $ACI_1$ and $BCI_2$ are $O_1$ and $O_2$ respectively. Prove that $I_1I_2$ and $O_1O_2$ are parallel.
AlphaGeometry formalization: a b c = triangle; d = foot a b c; e = foot b a c; f = foot c a b; i1 = incenter a e f; i2 = incenter b d f; o1 = circumcenter a c i1; o2 = circumcenter b c i2 ? para i1 i2 o1 o2
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; I1 = incenter A E F; I2 = incenter B D F; O1 = circumcenter A C I1; O2 = circumcenter B C I2; I1I2 = line I1 I2; O1O2 = line O1 O2; Prove: parallel I1I2 O1O2
Difficulty score: 3.0