Problem (2013USATSTp2): Let $ABC$ be a scalene triangle with $\angle BCA = 90^{\circ}$, and let $D$ be the foot of the altitude from $C$. Let $X$ be a point in the interior of the segment $CD$. Let $K$ be the point on the segment $AX$ such that $BK = BC$. Similarly, let $L$ be the point on the segment $BX$ such that $AL = AC$. The circumcircle of triangle $DKL$ intersects segment $AB$ at a second point $T$ (other than $D$). Prove that $\angle ACT = \angle BCT$.
AlphaGeometry formalization: c b a = r_triangle; d = foot c a b; x = on_line c d; k = on_line a x, eqdistance k b b c; l = on_line b x, eqdistance l a a c; o1 = circumcenter d k l; t = on_line a b, on_circle o1 d ? eqangle a c c t t c c b
HAGeo formalization: C A B = right_triangle; AB = line A B; D = foot C AB; CD = line C D; X = on_line CD; AX = line A X; (B,C) = circle_center_point B C; K = intersection AX (B,C); BX = line B X; (A,C) = circle_center_point A C; L = intersection BX (A,C); O1 = circumcenter D K L; (DKL) = circle_center_point O1 D; T = intersection AB (DKL); Prove: equal_angle A C T T C B
Difficulty score: 4.8