Problem (2017G5): Let $ABCC_1B_1A_1$ be a convex hexagon such that $AB=BC$, and suppose that the line segments $AA_1, BB_1$, and $CC_1$ have the same perpendicular bisector. Let the diagonals $AC_1$ and $A_1C$ meet at $D$, and denote by $\omega$ the circle $ABC$. Let $\omega$ intersect the circle $A_1BC_1$ again at $E \neq B$. Prove that the lines $BB_1$ and $DE$ intersect on $\omega$.
AlphaGeometry formalization: b a c = iso_triangle; p1 p2 = segment; a1 = reflect a p1 p2; b1 = reflect b p1 p2; c1 = reflect c p1 p2; d = on_line a c1, on_line a1 c; o1 = circumcenter a b c; o2 = circumcenter a1 b c1; e = on_circle o1 a, on_circle o2 b; x = on_line b b1, on_line d e ? cyclic x a b c
HAGeo formalization: l = line; B C A = isos_triangle; A1 = reflect A l; B1 = reflect B l; C1 = reflect C l; AC1 = line A C1; A1C = line A1 C; D = intersection AC1 A1C; O1 = circumcenter A B C; O2 = circumcenter A1 B C1; (A1BC1) = circle_center_point O2 B; (ABC) = circle_center_point O1 A; E = intersection (A1BC1) (ABC); BB1 = line B B1; DE = line D E; X = intersection BB1 DE; Prove: concyclic X A B C
Difficulty score: 4.1