Problem (2020IranGOAp2): Let $\triangle ABC$ be an acute-angled triangle with its incenter $I$. Suppose that $N$ is the midpoint of the arc $\overarc{BAC}$ of the circumcircle of triangle $\triangle ABC$, and $P$ is a point such that $ABPC$ is a parallelogram.Let $Q$ be the reflection of $A$ over $N$ and $R$ the projection of $A$ on $\overline{QI}$. Show that the line $\overline{AI}$ is tangent to the circumcircle of triangle $\triangle PQR$
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; o = circumcenter a b c; n = on_bline b c, on_circle o a; m = midpoint b c; p = mirror a m; q = mirror a n; r = foot a q i; o1 = circumcenter p q r; t = foot o1 a i ? cong o1 p o1 t
HAGeo formalization: A B C = acute_triangle; I = incenter A B C; O = circumcenter A B C; N = midarc B A C; M = midpoint B C; P = reflect A M; Q = reflect A N; IQ = line I Q; R = foot A IQ; AI = line A I; O1 = circumcenter P Q R; T = foot O1 AI; Prove: cong O1 P O1 T
Difficulty score: 3.3