Proving $L=\left\{ \left\langle M\right\rangle \mid L\left(M\right)=A_{TM}\right\} \in\overline{RE\cup coRE}$ I'd like to prove the following statement: 
$$L=\left\{ \left\langle M\right\rangle \mid L\left(M\right)=A_{TM}\right\} \in\overline{RE\cup coRE}$$
Where $$A_{TM}=\left\{ \left\langle M,w\right\rangle \mid M\text{ is a TM that accepts }w\right\} $$
Iv'e concluded the way to do this is to show a many-one reduction $$ALL_{TM}\leq_{m}L$$
where
$$ALL_{TM}=\left\{ \left\langle M\right\rangle \mid M\text{ is a TM with }L\left(M\right)=\Sigma^{*}\right\} $$
Since I know that $ALL_{TM}\in\overline{RE\cup coRE}$. But the level of recursion at this point is making my head spin. 
So my questions are:
1) Am I on the right track? is this reduction feasible?
2) If so, perhaps a hint on how to construct it?
Edit (Answer):
I ended up using a different approach. I showed the two many-one reductions $A_{TM}\leq_{m}L$ and $\overline{A_{TM}}\leq_{m}L$ which give the same result.
 A: There is a process that often makes problems of this sort much easier, and also gives a more precise computation of the level of uncomputability of a set. 
The first step in any problem like this is to use the Tarski-Kuratowski procedure to estimate how uncomputable the set is. To do this, we write down a definition of the set using quantifiers of the natural numbers and computable predicates. 
Let $H(M,w,s)$ be the computable predicate saying machine $M$ accepts $w$ after exactly $s$ steps. Then 
$$
A_{TM} = \{ \langle M,w\rangle | (\exists s)H(M,w,s) \}
$$
and so we have 
$$
N \in L \leftrightarrow (\forall M,w)(\forall s)\left [ [H(N, \langle M,w\rangle, s) \to (\exists s') H(M,w,s')] \\ \land [ H(M,w,s) \to (\exists s'') H(N, \langle M,w\rangle, s'')]\right ]
$$
We then put this in prenex form:
$$
N \in L \leftrightarrow (\forall M,w)(\forall s)(\exists s')(\exists s'')[ [H(N, \langle M,w\rangle, s) \to  H(M,w,s')]\\ \land [ H(M,w,s) \to  H(N, \langle M,w\rangle, s'')]]
$$
The resulting formula starts with a block of $\forall$ followed by a block of $\exists$, so it is at level $\Pi^0_2$ of the arithmetical hierarchy. This is an upper bound for the level of uncomputability of the set, but a surprising fact is that the level obtained by this process is usually the exact level of uncomputability of the language.
So we want to prove our language is $\Pi^0_2$ complete. Let $R(a,b,c)$ be any computable relation, and look at $S = \{ c : (\forall a)(\exists b)R(a,b,c)\}$. We want to prove that $S$ is many-one reducible to our original language - because $R$ is arbitrary, this shows our language is $\Pi^0_2$ complete.
To do this, start with a machine $M$ that is in $N$. Now, given a number $c$, we make a new machine $M'(c)$ as follows. For each input $v$ of length $n$, $M'(c)$ first searches for each $a < n$ for a $b$ such that $R(a,b,c)$. If it finds such a $b$ for each $a < n$, then $M'(c)$ runs $M$ on $v$ and returns whatever $M$ returns.  So, if  $(\forall a)(\exists b)R(a,b,c)$ then $M'(c)$ has the same behavior as $M$. However, if there is a $c$ so that $\lnot (\forall a)(\exists b)R(n,b,c)$ then $M'(c)$ will not have the same language as $M$, because $M'(c)$ will go into an infinite loop rather than accepting some inputs that $M$ would accept.
Overall, we have that $c \in S$ if and only if $M'(c) \in N$, so $N$ is a $\Pi^0_2$ complete set. In particular, by Post's theorem, this means $N$ is not r.e. (the r.e. sets are the $\Sigma^0_1$ sets) or co-r.e. (the co-r.e. sets are the $\Pi^0_1$ sets). 
A: EDIT: This approach doesn't work for this particular problem, but I'm leaving this answer here since it has some value in different settings.
I don't know whether the reduction you suggest is easy to construct. Here's an alternative approach:


*

*Show that $L$ is undecidable.

*Show that $L$ reduces to $\overline L$ and vice-versa. Therefore, $L$ is $\mathsf{RE}$ iff $L$ is $\mathsf{coRE}$.

*Recall that a language is in $\mathsf{RE} \cap \mathsf{coRE}$ precisely if it is decidable.

