Problem (2024SAGFp6): $BD$ is an altitude of $\triangle ABC$. $H$ is the orthocenter. $P$ is a point on $\odot(BC)$. Tangent of $\odot(BC)$ at $P$ intersects $BD$ at $Q$. $X$ is on line $AB$ and $PX\perp BC$. $PH, QX$ intersect at point $R$. Line $AR$ intersects $\odot(AH)$ again at $U$. Prove that $U,P,D,Q$ are concyclic.
AlphaGeometry formalization: a b c = triangle; d = foot b a c; h = orthocenter a b c; m1 = midpoint b c; p = on_circle m1 b; q = on_tline p m1 p, on_line b d; x = on_line a b, on_tline p b c; r = on_line p h, on_line q x; m2 = midpoint a h; u = on_line a r, on_circle m2 a ? cyclic u p d q
HAGeo formalization: A B C = triangle; AC = line A C; D = foot B AC; H = orthocenter A B C; M1 = midpoint B C; (BC) = circle_center_point M1 B; P = on_circle (BC); M1P = line M1 P; l1 = perpendicular_line P M1P; BD = line B D; Q = intersection l1 BD; BC = line B C; l2 = perpendicular_line P BC; AB = line A B; X = intersection AB l2; HP = line H P; QX = line Q X; R = intersection HP QX; AR = line A R; M2 = midpoint A H; (AH) = circle_center_point M2 A; U = intersection AR (AH); Prove: concyclic U P D Q
Difficulty score: 4.2