Problem (2006G4): A point $D$ is chosen on the side $AC$ of a triangle $ABC$ with $\angle C < \angle A < 90^\circ$ in such a way that $BD=BA$. The incircle of $ABC$ is tangent to $AB$ and $AC$ at points $K$ and $L$, respectively. Let $J$ be the incenter of triangle $BCD$. Prove that the line $KL$ intersects the line segment $AJ$ at its midpoint.
AlphaGeometry formalization: a b c = triangle; d = on_line a c, eqdistance d b b a; i = incenter a b c; k = foot i a b; l = foot i a c; j = incenter b c d; m = on_line k l, on_line a j ? midp m a j
HAGeo formalization: A B C = acute_triangle; AC = line A C; (B) = circle_center_point B A; D = intersection AC (B); I = incenter A B C; AB = line A B; K = foot I AB; L = foot I AC; J = incenter B C D; KL = line K L; AJ = line A J; M = intersection KL AJ; Prove: midpoint M A J
Difficulty score: 3.0