Problem (2014CGMOp6): In acute triangle $ABC$, $AB > AC$. $D$ and $E$ are the midpoints of $AB$, $AC$ respectively. The circumcircle of $ADE$ intersects the circumcircle of $BCE$ again at $P$. The circumcircle of $ADE$ intersects the circumcircle $BCD$ again at $Q$. Prove that $AP = AQ$.
AlphaGeometry formalization: a b c = triangle; d = midpoint a b; e = midpoint a c; o1 = circumcenter a d e; o2 = circumcenter b c e; p = on_circle o1 a, on_circle o2 b; o3 = circumcenter b c d; q = on_circle o1 a, on_circle o3 b ? cong a p a q
HAGeo formalization: A B C = acute_triangle; D = midpoint A B; E = midpoint A C; O1 = circumcenter A D E; (O1) = circle_center_point O1 A; O2 = circumcenter B C E; (O2) = circle_center_point O2 B; P = intersection (O1) (O2); O3 = circumcenter B C D; (O3) = circle_center_point O3 B; Q = intersection (O1) (O3); Prove: cong A P A Q
Difficulty score: 2.8