Problem (2013CGMOp2): As shown in the figure below, $ABCD$ is a trapezoid, $AB \parallel CD$. The sides $DA$, $AB$, $BC$ are tangent to $\odot O_1$ and $AB$ touches $\odot O_1$ at $P$. The sides $BC$, $CD$, $DA$ are tangent to $\odot O_2$, and $CD$ touches $\odot O_2$ at $Q$. Prove that the lines $AC$, $BD$, $PQ$ meet at the same point.
AlphaGeometry formalization: a b c d = trapezoid; e = on_line a d, on_line b c; o1 = excenter e a b; p = foot o1 a b; o2 = incenter e c d; q = foot o2 c d; x = on_line a c, on_line b d ? coll x p q
HAGeo formalization: A D C B = trapezoid; AD = line A D; BC = line B C; E = intersection AD BC; O1 = excenter E A B; AB = line A B; P = foot O1 AB; O2 = incenter E C D; CD = line C D; Q = foot O2 CD; AC = line A C; BD = line B D; PQ = line P Q; X = intersection AC BD; Prove: collinear X P Q
Difficulty score: 1.6