Is $L=\{\langle M\rangle\mid L(M)\subseteq HP\}\in coRE$? My intuition is that $L\notin coRE$, but I haven't managed to prove that $HP \le L$, as previously I only saw reductions from $HP$ or from $\overline{HP}$ with $f$ such that $f((\langle M\rangle,x))=\langle M_x\rangle$, while $M_x$ performs some simulation of $M$ on $x$.

(The answer eluded me for some time, so I started writing a question here. After I found the surprisingly simple answer, I decided to post it (Q&amp;A-style) anyway.)
We would show that $HP \le L$.

Let $f:\Sigma^*\rightarrow \Sigma^*$ be a function such that for any $x\in \Sigma^*$:
$$f(x)=\langle M_x\rangle$$
while $M_x$ is a TM that accepts $x$ and rejects every other word.

$f$ is computable, as it only requires writing the encoding of a very simple TM.

Now, for any $x\in \Sigma^*$:


$L(M_x)=\{x\}$
If $x\in HP$, then $\{x\}\subseteq HP$, and so $\langle M_x\rangle \in L$.
Otherwise, $x\notin HP$, and then $\{x\}\not\subseteq HP$, and so $\langle M_x\rangle \notin L$.


Therefore, indeed $HP \le L$.

Thus, it must be that $L\notin coRE$, because otherwise the reduction would imply that $HP\in coRE$, which is false.