Problem (2017ARMOg10p8): In a non-isosceles triangle $ABC$,$O$ and $I$ are circumcenter and incenter,respectively.$B^\prime$ is reflection of $B$ with respect to $OI$ and lies inside the angle $ABI$.Prove that the tangents to circumcirle of $\triangle BB^\prime I$ at $B^\prime$,$I$ intersect on $AC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; i = incenter a b c; b1 = reflect b o i; o1 = circumcenter b b1 i; t = on_tline b1 o1 b1, on_tline i o1 i ? coll a c t
HAGeo formalization: A B C = triangle; O = circumcenter A B C; I = incenter A B C; IO = line I O; B1 = reflect_point_wrt_line B IO; O1 = circumcenter B B1 I; O1B1 = line O1 B1; l1 = perpendicular_line B1 O1B1; O1I = line O1 I; l2 = perpendicular_line I O1I; T = intersection l1 l2; Prove: collinear A C T
Difficulty score: 3.2