Problem (ShuZhiMiGeo128): For point $P$ in $\triangle ABC$ with Cevian triangle $DEF$ and Miquel point $Q$ of $DEF$, take $R\in PQ$ with $AR\cap\odot(AEF)=J$, $BR\cap\odot(BFD)=K$, $CR\cap\odot(CDE)=L$. Prove $\odot(AJD)$, $\odot(BKE)$, $\odot(CLF)$ are coaxial.
AlphaGeometry formalization: a b c = triangle; p = free; d = on_line a p, on_line b c; e = on_line b p, on_line a c; f = on_line c p, on_line a b; o1 = circumcenter a e f; o2 = circumcenter b d f; q = on_circle o1 a, on_circle o2 b; r = on_line p q; j = on_line a r, on_circle o1 a; k = on_line b r, on_circle o2 b; o3 = circumcenter c d e; l = on_line c r, on_circle o3 c; oa = circumcenter a j d; ob = circumcenter b k e; t = on_circle oa a, on_circle ob b ? cyclic t c l f
HAGeo formalization: A B C = triangle; P = point; AP = line A P; BC = line B C; D = intersection AP BC; BP = line B P; AC = line A C; E = intersection BP AC; CP = line C P; AB = line A B; F = intersection CP AB; O1 = circumcenter A E F; O2 = circumcenter B D F; (O1) = circle_center_point O1 A; (O2) = circle_center_point O2 B; Q = intersection (O1) (O2); PQ = line P Q; R = on_line PQ; AR = line A R; J = intersection AR (O1); BR = line B R; K = intersection BR (O2); O3 = circumcenter C D E; CR = line C R; (O3) = circle_center_point O3 C; L = intersection CR (O3); Oa = circumcenter A J D; Ob = circumcenter B K E; (Oa) = circle_center_point Oa A; (Ob) = circle_center_point Ob B; T = intersection (Oa) (Ob); Prove: concyclic T C L F
Difficulty score: 6.4