[proofplan] We apply the one-prime form of [Ribet's level-lowering theorem](https://doi.org/10.1007/BF01389025). The hypotheses say precisely that the residual representation attached to $f$ is irreducible, has residue characteristic away from $p$, and has no local conductor contribution at the prime $p$ although $p$ occurs exactly once in the level of $f$. Ribet's criterion removes the $p$-factor from the tame level and produces a residual Hecke eigensystem at level $N/p$ with the same residual Galois representation; the [Deligne-Serre lifting lemma](https://doi.org/10.1007/BF02684334) realizes that eigensystem by a characteristic-zero eigenform, whose newform constituent has some level dividing $N/p$. [/proofplan] [step:Attach the residual Hecke eigensystem determined by $f$] Let $K_f$ be the coefficient field of $f$, let $\lambda$ be the prime of $K_f$ above $\ell$ occurring in $\bar{\rho}_{f,\lambda}$, and let $k_\lambda$ be its residue field. For every prime $q\nmid N\ell$, the residual representation \begin{align*} \bar{\rho}_{f,\lambda}: \operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) &\to GL_2(k_\lambda) \end{align*} is characterized by \begin{align*} \operatorname{tr}\bigl(\bar{\rho}_{f,\lambda}(\operatorname{Frob}_q)\bigr) &= a_q(f) \bmod \lambda, \\ \det\bigl(\bar{\rho}_{f,\lambda}(\operatorname{Frob}_q)\bigr) &= q \bmod \lambda, \end{align*} where $a_q(f)$ is the $q$-th Hecke eigenvalue of $f$ and $\operatorname{Frob}_q$ is an arithmetic Frobenius element at $q$. Define $\mathbb{T}_N$ to be the weight $2$ Hecke algebra of tame level $N$ and nebentypus $1$, generated over $\mathbb{Z}$ by the operators $T_q$ for $q\nmid N$ and $U_q$ for $q\mid N$. The form $f$ defines a homomorphism \begin{align*} \theta_f: \mathbb{T}_N &\to \mathcal{O}_{K_f} \\ T_q &\mapsto a_q(f) \end{align*} for $q\nmid N$, with the analogous $U_q$ eigenvalues at primes dividing $N$. Let $\mathfrak{m}_f$ be the maximal ideal of $\mathbb{T}_N$ obtained as the inverse image under $\theta_f$ of the prime ideal $\lambda\subset \mathcal{O}_{K_f}$. Thus $\mathfrak{m}_f$ records exactly the residual Hecke eigensystem attached to $\bar{\rho}_{f,\lambda}$. [/step] [step:Verify that the prime $p$ is removable by Ribet's criterion] We use the following one-prime form of [Ribet's level-lowering theorem](https://doi.org/10.1007/BF01389025) in weight $2$: if $p\ne \ell$, the exponent of $p$ in the level is $1$, the residual representation attached to the maximal Hecke ideal is irreducible, and the residual representation is unramified at $p$, then the same residual maximal ideal occurs in the Hecke algebra of level with the factor $p$ removed. The conclusion is a mod $\ell$ eigensystem at level $N/p$; after characteristic-zero lifting and newform decomposition, this gives a newform of some level dividing $N/p$, not necessarily exact level $N/p$. Its hypotheses are exactly the hypotheses in the theorem. The condition $p\ne \ell$ supplies the required distinction between the residue characteristic and the prime being lowered. The assumption that $p$ divides $N$ exactly once says that the $p$-part of the level is semistable, namely $v_p(N)=1$. The representation $\bar{\rho}_{f,\lambda}$ is irreducible by hypothesis, and it is unramified at $p$ by hypothesis. Therefore Ribet's criterion gives a maximal ideal $\mathfrak{m}'$ of the weight $2$ Hecke algebra $\mathbb{T}_{N/p}$ of level $N/p$ and nebentypus $1$ such that, for every prime $q\nmid N\ell$, \begin{align*} T_q \bmod \mathfrak{m}' = a_q(f) \bmod \lambda. \end{align*} Equivalently, the residual Hecke eigensystem determined by $\mathfrak{m}'$ agrees with the one determined by $\mathfrak{m}_f$ away from $N\ell$. [/step] [step:Lift the lowered residual eigensystem to a newform of level dividing $N/p$] The maximal ideal $\mathfrak{m}'\subset \mathbb{T}_{N/p}$ gives a system of Hecke eigenvalues over the finite field $\mathbb{T}_{N/p}/\mathfrak{m}'$. By the [Deligne-Serre lifting lemma](https://doi.org/10.1007/BF02684334) for weight $2$ modular forms, this mod $\ell$ eigensystem is lifted by a characteristic-zero normalized eigenform $h$ of weight $2$ and level $N/p$. Decompose $h$ using the oldform-newform decomposition at level $N/p$. Then some newform constituent $g$ has weight $2$ and level $M$ for a divisor $M\mid N/p$, and its Hecke eigenvalues reduce to the eigensystem defined by $\mathfrak{m}'$ at all primes away from $N\ell$. Let $K_g$ be the coefficient field of $g$, and choose a prime $\mu\subset \mathcal{O}_{K_g}$ above $\ell$ together with an embedding of the residue field $\mathcal{O}_{K_g}/\mu$ and $k_\lambda$ into a common finite extension of $\mathbb{F}_\ell$. With this comparison understood, we have \begin{align*} a_q(g) \equiv a_q(f) \pmod{\mu,\lambda} \end{align*} for every prime $q\nmid N\ell$. [/step] [step:Identify the residual Galois representations] For every prime $q\nmid N\ell$, the residual representations $\bar{\rho}_{g,\mu}$ and $\bar{\rho}_{f,\lambda}$ are both unramified at $q$ and, after the residue-field comparison fixed above, satisfy \begin{align*} \operatorname{tr}\bigl(\bar{\rho}_{g,\mu}(\operatorname{Frob}_q)\bigr) &= a_q(g) \bmod \mu = a_q(f) \bmod \lambda = \operatorname{tr}\bigl(\bar{\rho}_{f,\lambda}(\operatorname{Frob}_q)\bigr), \\ \det\bigl(\bar{\rho}_{g,\mu}(\operatorname{Frob}_q)\bigr) &= q \bmod \mu = q \bmod \lambda = \det\bigl(\bar{\rho}_{f,\lambda}(\operatorname{Frob}_q)\bigr). \end{align*} The set of such Frobenius conjugacy classes is dense in $\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ by the [Chebotarev density theorem](https://en.wikipedia.org/wiki/Chebotarev%27s_density_theorem). By the [Brauer-Nesbitt theorem](https://en.wikipedia.org/wiki/Brauer%E2%80%93Nesbitt_theorem), equality of characteristic polynomials on this dense set identifies the semisimplifications of the two residual representations. Since $\bar{\rho}_{f,\lambda}$ is irreducible, it is already semisimple, so \begin{align*} \bar{\rho}_{g,\mu}^{\mathrm{ss}}\cong \bar{\rho}_{f,\lambda}. \end{align*} This is the asserted weight $2$ newform of level $M$ with $M\mid N/p$. [/step]