Problem (2015IranTSTp18): $AH$ is the altitude of triangle $ABC$ and $H^\prime$ is the reflection of $H$ trough the midpoint of $BC$. If the tangent lines to the circumcircle of $ABC$ at $B$ and $C$, intersect each other at $X$ and the perpendicular line to $XH^\prime$ at $H^\prime$, intersects $AB$ and $AC$ at $Y$ and $Z$ respectively, prove that $\angle ZXC=\angle YXB$.
AlphaGeometry formalization: a b c = triangle; h = foot a b c; m_bc = midpoint b c; h1 = mirror h m_bc; o = circumcenter a b c; x = on_tline b o b, on_tline c o c; y = on_line a b, on_tline h1 x h1; z = on_line a c, on_tline h1 x h1 ? eqangle z x x c y x x b
HAGeo formalization: A B C = triangle; BC = line B C; H = foot A BC; M_bc = midpoint B C; H1 = reflect_point_wrt_point H M_bc; O = circumcenter A B C; OB = line O B; l1 = perpendicular_line B OB; OC = line O C; l2 = perpendicular_line C OC; X = intersection l1 l2; AB = line A B; XH1 = line X H1; l3 = perpendicular_line H1 XH1; Y = intersection AB l3; AC = line A C; Z = intersection AC l3; Prove: equal_angle Z X C Y X B
Difficulty score: 4.1