Problem (2021IranGOAp5a): Given a triangle $ABC$ with incenter $I$. The incircle of triangle $ABC$ is tangent to $BC$ at $D$. Let $P$ and $Q$ be points on the side BC such that $\angle PAB = \angle BCA$ and $\angle QAC = \angle ABC$, respectively. Let $K$ and $L$ be the incenter of triangles $ABP$ and $ACQ$, respectively. Prove that $AD$ is the Euler line of triangle $IKL$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; p = on_line b c, on_aline p a b b c a; q = on_line b c, on_aline q a c c b a; k = incenter a b p; l = incenter a c q; o1 = circumcenter i k l; h1 = orthocenter i k l ? coll a d o1
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; D = foot I BC; l1 = angle_equal1 A B B C A; P = intersection BC l1; l2 = angle_equal1 A C C B A; Q = intersection BC l2; K = incenter A B P; L = incenter A C Q; O1 = circumcenter I K L; H1 = orthocenter I K L; Prove: collinear A D O1
Difficulty score: 5.1