Problem (2014ARMOg9p6): Let $ABCD$ be a trapezoid with $AB\parallel CD$ and $ \Omega $ is a circle passing through $A,B,C,D$. Let $ \omega $ be the circle passing through $C,D$ and intersecting with $CA,CB$ at $A_1$, $B_1$ respectively. $A_2$ and $B_2$ are the points symmetric to $A_1$ and $B_1$ respectively, with respect to the midpoints of $CA$ and $CB$. Prove that the points $A,B,A_2,B_2$ are concyclic.
AlphaGeometry formalization: a b c d = eq_trapezoid; o = on_bline c d; a1 = on_line a c, on_circle o c; b1 = on_line b c, on_circle o c; m1 = midpoint c a; m2 = midpoint c b; a2 = mirror a1 m1; b2 = mirror b1 m2 ? cyclic a b a2 b2
HAGeo formalization: A D C B = isos_trapezoid; l = perpendicular_bisector C D; O = on_line l; (O) = circle_center_point O C; AC = line A C; A1 = intersection AC (O); BC = line B C; B1 = intersection BC (O); M1 = midpoint C A; M2 = midpoint C B; A2 = reflect_point_wrt_point A1 M1; B2 = reflect_point_wrt_point B1 M2; Prove: concyclic A B A2 B2
Difficulty score: 1.0