Problem (2022ARMOg10p2): On side $BC$ of an acute triangle $ABC$ are marked points $D$ and $E$ so that $BD = CE$. On the arc $DE$ of the circumscribed circle of triangle $ADE$ that does not contain the point $A$, there are points $P$ and $Q$ such that $AB = PC$ and $AC = BQ$. Prove that $AP=AQ$.
AlphaGeometry formalization: a b c = triangle; d = on_line b c; m = midpoint b c; e = mirror d m; o1 = circumcenter a d e; p = on_circle o1 a, eqdistance p c a b; q = on_circle o1 a, eqdistance q b a c ? cong a p a q
HAGeo formalization: A B C = acute_triangle; BC = line B C; D = on_line BC; M = midpoint B C; E = reflect_point_wrt_point D M; O1 = circumcenter A D E; (O1) = circle_center_point O1 A; (C,AB) = circle_center_radius C A B; P = intersection (O1) (C,AB); (B,AC) = circle_center_radius B A C; Q = intersection (O1) (B,AC); Prove: cong A P A Q
Difficulty score: 2.6