Problem (2019ELMOSLp4): Let triangle $ABC$ have altitudes $BE$ and $CF$ which meet at $H$. The reflection of $A$ over $BC$ is $A'$. Let $(ABC)$ meet $(AA'E)$ at $P$ and $(AA'F)$ at $Q$. Let $BC$ meet $PQ$ at $R$. Prove that $EF \parallel HR$.
AlphaGeometry formalization: a b c = triangle; e = foot b a c; f = foot c a b; h = on_line b e, on_line c f; a1 = reflect a b c; o = circumcenter a b c; o1 = circumcenter a a1 e; o2 = circumcenter a a1 f; p = on_circle o a, on_circle o1 a; q = on_circle o a, on_circle o2 a; r = on_line b c, on_line p q ? para e f h r
HAGeo formalization: A B C = triangle; AC = line A C; E = foot B AC; AB = line A B; F = foot C AB; H = orthocenter A B C; BC = line B C; A1 = reflect_point_wrt_line A BC; O = circumcenter A B C; O1 = circumcenter A A1 E; O2 = circumcenter A A1 F; (ABC) = circle_center_point O A; (AA1E) = circle_center_point O1 A; P = intersection (ABC) (AA1E); (AA1F) = circle_center_point O2 A; Q = intersection (ABC) (AA1F); PQ = line P Q; R = intersection BC PQ; EF = line E F; HR = line H R; Prove: parallel EF HR
Difficulty score: 4.7