Problem (2016ELMOp2): Oscar is drawing diagrams with trash can lids and sticks. He draws a triangle $ABC$ and a point $D$ such that $DB$ and $DC$ are tangent to the circumcircle of $ABC$. Let $B'$ be the reflection of $B$ over $AC$ and $C'$ be the reflection of $C$ over $AB$. If $O$ is the circumcenter of $DB'C'$, help Oscar prove that $AO$ is perpendicular to $BC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_tline b o b, on_tline c o c; b1 = reflect b a c; c1 = reflect c a b; o1 = circumcenter d b1 c1 ? perp a o1 b c
HAGeo formalization: A B C = triangle; O = circumcenter A B C; OB = line O B; OC = line O C; l1 = perpendicular_line B OB; l2 = perpendicular_line C OC; D = intersection l1 l2; AC = line A C; B1 = reflect_point_wrt_line B AC; AB = line A B; C1 = reflect_point_wrt_line C AB; O1 = circumcenter D B1 C1; AO1 = line A O1; BC = line B C; Prove: perpendicular AO1 BC
Difficulty score: 2.9