Problem (2016CTSTp7): $P$ is a point in the interior of acute triangle $ABC$. $D,E,F$ are the reflections of $P$ across $BC,CA,AB$ respectively. Rays $AP,BP,CP$ meet the circumcircle of $\triangle ABC$ at $L,M,N$ respectively. Prove that the circumcircles of $\triangle PDL,\triangle PEM,\triangle PFN$ meet at a point $T$ different from $P$.
AlphaGeometry formalization: a b c = triangle; p = free; d = reflect p b c; e = reflect p c a; f = reflect p a b; o = circumcenter a b c; l = on_line a p, on_circle o a; m = on_line b p, on_circle o a; n = on_line c p, on_circle o a; o1 = circumcenter p d l; o2 = circumcenter p e m; t = on_circle o1 p, on_circle o2 p ? cyclic t p f n
HAGeo formalization: A B C = acute_triangle; P = point; BC = line B C; D = reflect_point_wrt_line P BC; AC = line A C; E = reflect_point_wrt_line P AC; AB = line A B; F = reflect_point_wrt_line P AB; AP = line A P; O = circumcenter A B C; (O) = circle_center_point O A; L = intersection AP (O); BP = line B P; M = intersection BP (O); CP = line C P; N = intersection CP (O); O1 = circumcenter D L P; (O1) = circle_center_point O1 P; O2 = circumcenter E M P; (O2) = circle_center_point O2 P; X = intersection (O1) (O2); Prove: concyclic X F N P
Difficulty score: 3.9