Problem (2012USATSTp6): In cyclic quadrilateral $ABCD$, diagonals $AC$ and $BD$ intersect at $P$. Let $E$ and $F$ be the respective feet of the perpendiculars from $P$ to lines $AB$ and $CD$. Segments $BF$ and $CE$ meet at $Q$. Prove that lines $PQ$ and $EF$ are perpendicular to each other.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; p = on_line a c, on_line b d; e = foot p a b; f = foot p c d; q = on_line b f, on_line c e ? perp p q e f
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); AC = line A C; BD = line B D; P = intersection AC BD; AB = line A B; E = foot P AB; CD = line C D; F = foot P CD; BF = line B F; CE = line C E; Q = intersection BF CE; PQ = line P Q; EF = line E F; Prove: perpendicular PQ EF
Difficulty score: 4.0