Problem (2023SAGFp8): On Circumcircle of $\Delta ABC$ , $D,E,F$ are midpoint of arcs $BC,CA,AB$ not containing the vertices. $R,S,T$ antipodes of $D,E,F$. $D',E',F'$ are reflections of $D,E,F$ across $BC,CA,AB$ and $R',S',T'$ are reflections of $R,S,T$ across $BC,CA,AB$. Let $H_1$ be orthocenter $\Delta D'E'F'$ and $O_1$ be circumcenter of $\Delta R'S'T'$. Prove that is the Euler line of $\Delta ABC\parallel  H_1O_1$.  $(b)$ $H_2 - $ be orthocenter $\Delta R'S'T'$,$O_2$ - be circumcenter of $\Delta D'E'F'$. Prove it: $H_1O_1 \parallel O_2H_2$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_bline b c, on_circle o a; e = on_bline c a, on_circle o a; f = on_bline a b, on_circle o a; r = mirror d o; s = mirror e o; t = mirror f o; d1 = reflect d b c; e1 = reflect e c a; f1 = reflect f a b; r1 = reflect r b c; s1 = reflect s c a; t1 = reflect t a b; h1 = orthocenter d1 e1 f1; o1 = circumcenter r1 s1 t1; h = orthocenter a b c ? para h1 o1 o h
HAGeo formalization: A B C = triangle; O = circumcenter A B C; D = midarc_no B C A; E = midarc_no C A B; F = midarc_no A B C; R = reflect D O; S = reflect E O; T = reflect F O; BC = line B C; CA = line C A; AB = line A B; D1 = reflect_point_wrt_line D BC; E1 = reflect_point_wrt_line E CA; F1 = reflect_point_wrt_line F AB; R1 = reflect_point_wrt_line R BC; S1 = reflect_point_wrt_line S CA; T1 = reflect_point_wrt_line T AB; H1 = orthocenter D1 E1 F1; O1 = circumcenter R1 S1 T1; H = orthocenter A B C; HO = line H O; H1O1 = line H1 O1; Prove: parallel HO H1O1
Difficulty score: 5.9