Ramanujan–Petersson conjecture for holomorphic cusp forms

Let $\Gamma\subseteq SL(2,\mathbb Z)$ be a congruence subgroup (it contains $\Gamma(N)$ for some $N\ge1$), let $k\ge1$ be an integer, and let $f$ be a holomorphic cusp form of weight $k$ for $\Gamma$. Let $h>0$ be the width of the cusp $\infty$ for $\Gamma$ and write $f(z)=\sum_{n\ge0}a_n e^{2\pi i n z/h}$. Then for every $\varepsilon>0$,

This is the Ramanujan–Petersson conjecture for holomorphic cusp forms, proved by Deligne for $k\ge2$ and by Deligne–Serre for $k=1$. For $\Delta$ ($k=12$, $\Gamma=SL(2,\mathbb Z)$) it gives $\tau(n)=O(n^{11/2+\varepsilon})$.

Formalization Note $\Gamma$ is mapped into $GL(2,\mathbb R)$, $f$ is a Mathlib CuspForm, and $a_n$ is the $n$-th coefficient of qExpansion with period $h=$ strictWidthInfty of $\Gamma$. This period equals $1$ when $z\mapsto z+1$ lies in $\Gamma$, for example for $\Gamma_0(N)$ and $\Gamma_1(N)$, so there $a_n$ are the usual coefficients in $q=e^{2\pi iz}$.