Problem (2017CHNGaoLian): Given an isocleos triangle $ABC$ with equal sides $AB=AC$ and incenter $I$.Let $\Gamma_1$be the circle centered at $A$ with radius $AB$,$\Gamma_2$ be the circle centered at $I$ with radius $BI$.A circle $\Gamma_3$ passing through $B,I$ intersects $\Gamma_1$,$\Gamma_2$ again at $P,Q$ (different from $B$) respectively.Let $R$ be the intersection of $PI$ and $BQ$.Show that $BR \perp CR$.
AlphaGeometry formalization: a b c = iso_triangle; i = incenter a b c; o3 = on_bline b i; p = on_circle a b, on_circle o3 b; q = on_circle i b, on_circle o3 b; r = on_line p i, on_line b q ? perp b r c r
HAGeo formalization: A B C = isos_triangle; I = incenter A B C; l = perpendicular_bisector B I; O3 = on_line l; (A) = circle_center_point A B; (A) = circle_center_point A B; (I) = circle_center_point I B; (O3) = circle_center_point O3 B; P = intersection (O3) (A); Q = intersection (O3) (I); IP = line I P; BQ = line B Q; R = intersection IP BQ; BR = line B R; CR = line C R; Prove: perpendicular BR CR
Difficulty score: 2.6