Problem (2021KoMaLA796): Let $ABCD$ be a cyclic quadrilateral. Let lines $AB$ and $CD$ intersect in $P,$ and lines $BC$ and $DA$ intersect in $Q.$ The feet of the perpendiculars from $P$ to $BC$ and $DA$ are $K$ and $L,$ and the feet of the perpendiculars from $Q$ to $AB$ and $CD$ are $M$ and $N.$ The midpoint of diagonal $AC$ is $F.$ Prove that the circumcircles of triangles $FKN$ and $FLM,$ and the line $PQ$ are concurrent.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; p = on_line a b, on_line c d; q = on_line b c, on_line d a; k = foot p b c; l = foot p d a; m = foot q a b; n = foot q c d; f = midpoint a c; r = on_circum f k n, on_circum f l m ? coll r p q
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); AB = line A B; CD = line C D; P = intersection AB CD; BC = line B C; AD = line A D; Q = intersection BC AD; K = foot P BC; L = foot P AD; M = foot Q AB; N = foot Q CD; F = midpoint A C; (FKN) = circle F K N; (FLM) = circle F L M; X = intersection (FKN) (FLM); Prove: collinear X P Q
Difficulty score: 3.5