Problem (2024IranTSTp2): For a right angled triangle $\triangle ABC$ with $\angle A=90$ we have $AC=2AB$. Point $M$ is the midpoint of side $BC$ and $I$ is incenter of triangle $\triangle ABC$. The line passing trough $M$ and perpendicular to $BI$ intersect with lines $BI$ and $AC$ at points $H$ and $K$ respectively. If the semi-line $IK$ cuts circumcircle of triangle $\triangle ABC$ at $F$ and $S$ be the second intersection point of line $FH$ with circumcircle of triangle $\triangle ABC$ , then prove that $SM$ is tangent to the incircle of triangle $\triangle ABC$.
AlphaGeometry formalization: a b x = risos; c = mirror a x; m = midpoint b c; i = incenter a b c; h = foot m b i; k = on_tline m b i, on_line a c; f = on_line i k, on_circle m a; s = on_line f h, on_circle m a; d = foot i a b; t = foot i s m ? cong i t i d
HAGeo formalization: A B X = right_isos_triangle A B X; C = reflect_point_wrt_point A X; M = midpoint B C; I = incenter A B C; BI = line B I; H = foot M BI; l1 = perpendicular_line M BI; AC = line A C; K = intersection l1 AC; IK = line I K; (ABC) = circle_center_point M A; F = intersection IK (ABC); FH = line F H; S = intersection FH (ABC); AB = line A B; D = foot I AB; SM = line S M; T = foot I SM; Prove: cong I T I D
Difficulty score: 4.1