Problem (2020RMMSLG3): In the triangle $ABC$ with circumcircle $\Gamma$, the incircle $\omega$ touches sides $BC, CA$, and $AB$ at $D, E$, and $F$, respectively. The line through $D$ perpendicular to $EF$ meets $\omega$ at $K\neq D$. Line $AK$ meets $\Gamma$ at $L\neq A$. Rays $KI$ and $IL$ meet the circumcircle of triangle $BIC$ at $Q\neq I$ and $P\neq I$, respectively. The circumcircles of triangles $KFB$ and $KEC$ meet $EF$ at $R\neq F$ and $S\neq E$, respectively. Prove that $PQRS$ is cyclic.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; i = incenter a b c; d = foot i b c; e = foot i a c; f = foot i a b; k = on_tline d e f, on_circle i d; l = on_line a k, on_circle o a; o1 = circumcenter b i c; q = on_line k i, on_circle o1 b; p = on_line i l, on_circle o1 b; o2 = circumcenter k f b; r = on_line e f, on_circle o2 k; o3 = circumcenter k e c; s = on_line e f, on_circle o3 k ? cyclic p q r s
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; AC = line A C; AB = line A B; D = foot I BC; E = foot I AC; F = foot I AB; (I) = circle_center_point I D; EF = line E F; l1 = perpendicular_line D EF; K = intersection l1 (I); AK = line A K; O = circumcenter A B C; (ABC) = circle_center_point O A; L = intersection AK (ABC); IK = line I K; O1 = circumcenter B C I; (BCI) = circle_center_point O1 B; Q = intersection IK (BCI); IL = line I L; P = intersection IL (BCI); O2 = circumcenter B F K; (BFK) = circle_center_point O2 B; R = intersection (BFK) EF; O3 = circumcenter C E K; (CEK) = circle_center_point O3 C; S = intersection (CEK) EF; Prove: concyclic P Q R S
Difficulty score: 4.0