Problem (2021IranTSTp6): Point $D$ is chosen on the Euler line of triangle $ABC$ and it is inside of the triangle. Points $E,F$ are were the line $BD,CD$ intersect with $AC,AB$ respectively. Point $X$ is on the line $AD$ such that $\angle EXF =180 - \angle A$, also $A,X$ are on the same side of $EF$. If $P$ is the second intersection of circumcircles of $CXF,BXE$ then prove the lines $XP,EF$ meet on the altitude of $A$
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; d = on_line o h; e = on_line b d, on_line a c; f = on_line c d, on_line a b; x = on_line a d, eqangle3 x e f a b c; o1 = circumcenter c x f; o2 = circumcenter b x e; p = on_circle o1 c, on_circle o2 b; q = on_line x p, on_line e f ? coll q a h
HAGeo formalization: A B C = triangle; O = circumcenter A B C; H = orthocenter A B C; OH = line O H; D = on_line OH; BD = line B D; AC = line A C; E = intersection BD AC; CD = line C D; AB = line A B; F = intersection CD AB; AD = line A D; ω1 = angle_equal2 E F B A C; X = intersection AD ω1; O1 = circumcenter C X F; O2 = circumcenter B X E; (O1) = circle_center_point O1 C; (O2) = circle_center_point O2 B; P = intersection (O1) (O2); XP = line X P; EF = line E F; Q = intersection XP EF; Prove: collinear Q A H
Difficulty score: 6.1