Problem (2020CSMGOp3): Let $\triangle ABC$ be a scalene triangle with the orthocenter $H$. Let $B'$ be the reflection of $B$ over $AC$ and $C'$ be the reflection of $C$ over $AB$. Let the tangents to the circumcircle of $\triangle ABC$ at points $B$ and $C$ meet at a point $X$. Suppose that the lines $B'C'$ and $BC$ meet at a point $T$. Prove that $AT$ is perpendicular to $XH$.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; b1 = reflect b a c; c1 = reflect c a b; o = circumcenter a b c; x = on_tline b o b, on_tline c o c; t = on_line b1 c1, on_line b c ? perp a t x h
HAGeo formalization: A B C = triangle; H = orthocenter A B C; AC = line A C; B1 = reflect_point_wrt_line B AC; AB = line A B; C1 = reflect_point_wrt_line C AB; O = circumcenter A B C; OB = line O B; OC = line O C; l1 = perpendicular_line B OB; l2 = perpendicular_line C OC; X = intersection l1 l2; B1C1 = line B1 C1; BC = line B C; T = intersection B1C1 BC; AT = line A T; HX = line H X; Prove: perpendicular AT HX
Difficulty score: 4.0