Problem (2015ARMOg9p7): An acute-angled $ABC \ (AB<AC)$ is inscribed into a circle $\omega$. Let $M$ be the centroid of $ABC$, and let $AH$ be an altitude of this triangle. A ray $MH$ meets $\omega$ at $A'$. Prove that the circumcircle of the triangle $A'HB$ is tangent to $AB$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; x y z m = centroid a b c; h = foot a b c; a1 = on_line m h, on_circle o a; o1 = circumcenter a1 h b ? perp o1 b a b
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; (O) = circle_center_point O A; M X Y Z = centroid A B C; BC = line B C; H = foot A BC; HM = line H M; A1 = intersection HM (O); O1 = circumcenter A1 B H; O1B = line O1 B; AB = line A B; Prove: perpendicular O1B AB
Difficulty score: 2.3