Problem (2020G6): Let $ABC$ be a triangle with $AB < AC$, incenter $I$, and $A$ excenter $I_{A}$. The incircle meets $BC$ at $D$. Define $E = AD\cap BI_{A}$, $F = AD\cap CI_{A}$. Show that the circumcircle of $\triangle AID$ and $\triangle I_{A}EF$ are tangent to each other
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; i1 = excenter a b c; d = foot i b c; e = on_line a d, on_line b i1; f = on_line a d, on_line c i1; o1 = circumcenter a i d; o2 = circumcenter i1 e f; t = on_circle o1 a, on_circle o2 i1 ? coll o1 o2 t
HAGeo formalization: A B C = triangle; I = incenter A B C; Ia = excenter A B C; BC = line B C; D = foot I BC; AD = line A D; BIa = line B Ia; E = intersection AD BIa; CIa = line C Ia; F = intersection AD CIa; O1 = circumcenter A I D; O2 = circumcenter Ia E F; (ADI) = circle_center_point O1 A; (EFIa) = circle_center_point O2 Ia; T = intersection (ADI) (EFIa); Prove: collinear O1 O2 T
Difficulty score: 3.3