Problem (2014IranTSTp13): The incircle of a non-isosceles triangle $ABC$ with the center $I$ touches the sides $BC,AC,AB$ at $A_{1},B_{1},C_{1}$ . let $AI,BI,CI$ meets $BC,AC,AB$ at $A_{2},B_{2},C_{2}$. let $A'$ is a point on $AI$ such that $A_{1}A'\perp B_{2}C_{2}$ .$B',C'$ respectively. prove that two triangle $A'B'C',A_{1}B_{1}C_{1}$ are equal.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; a1 = foot i b c; b1 = foot i a c; c1 = foot i a b; a2 = on_line b c, on_line a i; b2 = on_line a c, on_line b i; c2 = on_line a b, on_line c i; a3 = on_line a i, on_tline a1 b2 c2; b3 = on_line b i, on_tline b1 c2 a2; c3 = on_line c i, on_tline c1 a2 b2 ? contri a3 b3 c3 a1 b1 c1
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; AC = line A C; AB = line A B; A1 = foot I BC; B1 = foot I AC; C1 = foot I AB; BC = line B C; AI = line A I; A2 = intersection BC AI; AC = line A C; BI = line B I; B2 = intersection AC BI; AB = line A B; CI = line C I; C2 = intersection AB CI; B2C2 = line B2 C2; l1 = perpendicular_line A1 B2C2; A3 = intersection AI l1; C2A2 = line C2 A2; l2 = perpendicular_line B1 C2A2; B3 = intersection BI l2; A2B2 = line A2 B2; l3 = perpendicular_line C1 A2B2; C3 = intersection CI l3; Prove: congurrent A3 B3 C3 A1 B1 C1
Difficulty score: 4.5