Problem (2023USAMOp6): Let $ABC$ be a triangle with incenter $I$ and excenters $I_a$, $I_b$, and $I_c$ opposite $A$, $B$, and $C$, respectively. Let $D$ be an arbitrary point on the circumcircle of $\triangle{ABC}$ that does not lie on any of the lines $II_a$, $I_bI_c$, or $BC$. Suppose the circumcircles of $\triangle{DII_a}$ and $\triangle{DI_bI_c}$ intersect at two distinct points $D$ and $F$. If $E$ is the intersection of lines $DF$ and $BC$, prove that $\angle{BAD} = \angle{EAC}$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; ia = excenter a b c; ib = excenter b c a; ic = excenter c a b; o = circumcenter a b c; d = on_circle o a; o1 = circumcenter d i ia; o2 = circumcenter d ib ic; f = on_circle o1 d, on_circle o2 d; e = on_line d f, on_line b c ? eqangle b a a d e a a c
HAGeo formalization: A B C = triangle; I = incenter A B C; Ia = excenter A B C; Ib = excenter B C A; Ic = excenter C A B; O = circumcenter A B C; (ABC) = circle_center_point O A; D = on_circle (ABC); O1 = circumcenter D I Ia; O2 = circumcenter D Ib Ic; (DIIa) = circle_center_point O1 D; (DIbIc) = circle_center_point O2 D; F = intersection (DIIa) (DIbIc); DF = line D F; BC = line B C; E = intersection DF BC; Prove: equal_angle B A D E A C
Difficulty score: 4.5