Problem (2019ARMOg10p4): Let $ABC$ be an acute-angled triangle with $AC<BC.$ A circle passes through $A$ and $B$ and crosses the segments $AC$ and $BC$ again at $A_1$ and $B_1$ respectively. The circumcircles of $A_1B_1C$ and $ABC$ meet each other at points $P$ and $C.$ The segments $AB_1$ and $A_1B$ intersect at $S.$ Let $Q$ and $R$ be the reflections of $S$ in the lines $CA$ and $CB$ respectively. Prove that the points $P,$ $Q,$ $R,$ and $C$ are concyclic.
AlphaGeometry formalization: a b c = triangle; o = on_bline a b; a1 = on_line a c, on_circle o a; b1 = on_line b c, on_circle o a; o1 = circumcenter a1 b1 c; o2 = circumcenter a b c; p = on_circle o1 a1, on_circle o2 a; s = on_line a b1, on_line b a1; q = reflect s a c; r = reflect s b c ? cyclic p q r c
HAGeo formalization: A B C = acute_triangle; l = perpendicular_bisector A B; O = on_line l; ω = circle_center_point O A; AC = line A C; A1 = intersection ω AC; BC = line B C; B1 = intersection ω BC; O1 = circumcenter A1 B1 C; (A1B1C) = circle_center_point O1 A1; O2 = circumcenter A B C; (ABC) = circle_center_point O2 A; P = intersection (A1B1C) (ABC); AB1 = line A B1; A1B = line A1 B; S = intersection AB1 A1B; Q = reflect_point_wrt_line S AC; R = reflect_point_wrt_line S BC; Prove: concyclic P Q R C
Difficulty score: 3.1