Problem (2004CTSTp1): Using $ AB$ and $ AC$ as diameters, two semi-circles are constructed respectively outside the acute triangle $ ABC$. $ AH \perp BC$ at $ H$, $ D$ is any point on side $ BC$ ($ D$ is not coinside with $ B$ or $ C$ ), through $ D$, construct $ DE \parallel AC$ and $ DF \parallel AB$ with $ E$ and $ F$ on the two semi-circles respectively. Show that $ D$, $ E$, $ F$ and $ H$ are concyclic.
AlphaGeometry formalization: a b c = triangle; o1 = midpoint a b; o2 = midpoint a c; h = foot a b c; d = on_line b c; e = on_circle o1 a, on_pline d a c; f = on_circle o2 a, on_pline d a b ? cyclic d e f h
HAGeo formalization: A B C = acute_triangle; BC = line B C; H = foot A BC; D = on_line BC; AC = line A C; l1 = parallel_line D AC; O1 = midpoint A B; (O1) = circle_center_point O1 A; E = intersection l1 (O1); AB = line A B; l2 = parallel_line D AB; O2 = midpoint A C; (O2) = circle_center_point O2 A; F = intersection l2 (O2); Prove: concyclic D E F H
Difficulty score: 2.3