Problem (2020RMMp1): Let $ABC$ be a triangle with a right angle at $C$. Let $I$ be the incentre of triangle $ABC$, and let $D$ be the foot of the altitude from $C$ to $AB$. The incircle $\omega$ of triangle $ABC$ is tangent to sides $BC$, $CA$, and $AB$ at $A_1$, $B_1$, and $C_1$, respectively. Let $E$ and $F$ be the reflections of $C$ in lines $C_1A_1$ and $C_1B_1$, respectively. Let $K$ and $L$ be the reflections of $D$ in lines $C_1A_1$ and $C_1B_1$, respectively. Prove that the circumcircles of triangles $A_1EI$, $B_1FI$, and $C_1KL$ have a common point.
AlphaGeometry formalization: c a b = r_triangle; i = incenter c a b; d = foot c a b; a1 = foot i b c; b1 = foot i a c; c1 = foot i a b; e = reflect c c1 a1; f = reflect c c1 b1; k = reflect d c1 a1; l = reflect d c1 b1; p = on_circum a1 e i, on_circum b1 f i ? cyclic p c1 k l
HAGeo formalization: C A B = right_triangle; I = incenter A B C; AB = line A B; D = foot C AB; BC = line B C; A1 = foot I BC; AC = line A C; B1 = foot I AC; C1 = foot I AB; A1C1 = line A1 C1; E = reflect_point_wrt_line C A1C1; B1C1 = line B1 C1; F = reflect_point_wrt_line C B1C1; K = reflect_point_wrt_line D A1C1; L = reflect_point_wrt_line D B1C1; (A1EI) = circle A1 E I; (B1FI) = circle B1 F I; P = intersection (A1EI) (B1FI); Prove: concyclic P C1 K L
Difficulty score: 3.5