Problem (2009ARMOg11p7): Let be given a parallelogram $ ABCD$ and two points $ A_1$, $ C_1$ on its sides $ AB$, $ BC$, respectively. Lines $ AC_1$ and $ CA_1$ meet at $ P$. Assume that the circumcircles of triangles $ AA_1P$ and $ CC_1P$ intersect at the second point $ Q$ inside triangle $ ACD$. Prove that $ \angle PDA = \angle QBA$.
AlphaGeometry formalization: a b c = triangle; d = parallelogram a b c d; a1 = on_line a b; c1 = on_line b c; p = on_line a c1, on_line c a1; q = on_circum a a1 p, on_circum c c1 p ? eqangle p d d a a b b q
HAGeo formalization: A B C D = parallelogram; AB = line A B; A1 = on_line AB; BC = line B C; C1 = on_line BC; AC1 = line A C1; A1C = line A1 C; P = intersection AC1 A1C; (AA1P) = circle A A1 P; (CC1P) = circle C C1 P; Q = intersection (AA1P) (CC1P); Prove: equal_angle P D A A B Q
Difficulty score: 2.5