Problem (2024TurkeyMO2ndRp2): Let $\triangle ABC$ be an acute triangle, where $H$ is the orthocenter and $D,E,F$ are the feet of the altitudes from $A,B,C$ respectively. A circle tangent to $(DEF)$ at $D$ intersects the line $EF$ at $P$ and $Q$. Let $R$ and $S$ be the second intersection points of the circumcircle of triangle $\triangle BHC$ with $PH$ and $QH$, respectively. Let $T$ be the point on the line $BC$ such that $AT\perp EF$. Prove that the points $R,S,D,T$ are concyclic.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; d = foot a b c; e = foot b a c; f = foot c a b; o1 = circumcenter d e f; o2 = on_line o1 d; p = on_circle o2 d, on_line e f; q = on_circle o2 d, on_line e f; o3 = circumcenter b h c; r = on_line p h, on_circle o3 b; s = on_line q h, on_circle o3 b; t = on_line b c, on_tline a e f ? cyclic r s d t
HAGeo formalization: A B C = triangle; H = orthocenter A B C; BC = line B C; AC = line A C; AB = line A B; D = foot A BC; E = foot B AC; F = foot C AB; O1 = circumcenter D E F; O1D = line O1 D; O2 = on_line O1D; (O2) = circle_center_point O2 D; EF = line E F; P = intersection (O2) EF; Q = intersection (O2) EF; O3 = circumcenter B H C; PH = line P H; (O3) = circle_center_point O3 B; R = intersection PH (O3); QH = line Q H; S = intersection QH (O3); l1 = perpendicular_line A EF; T = intersection BC l1; Prove: concyclic R S D T
Difficulty score: 4.2