Proof-verification: Existence of an explicit formality morphism from the Barratt-Eccles Koszul dual cooperad

I know asking for proof-verification on MO is a tricky thing. On one hand interesting research level proofs are usually subject of articles and can not be discussed here in detail. On the other hand most simple proof which can be written on a forum are not "high-level" enough for MO and other places are more appropriate. After all MO does not have a "proof-verification" tag, like math.stackexchange.

Anyway, for my personal taste at least, the following is research level. So lets see where this goes:

I want to proof the following statement:

Consider everything over the field $\mathbb{Q}$. For a fixed, given $n\geq 2$, let $\mathcal{E}_{n}$ be the $E_{n}$-suboperad of the Barratt-Eccles operad $\mathcal{E}$, $\mathcal{E}_{n}^{i}$ its Koszul dual cooperad in the sense described in the paper "Koszul duality of En-operads" by Benoit Fresse and let $e_{n}$ be the operad of $(n-1)$-Gerstenhaber algebras. Then there exist a solution to the Maurer Cartan equation in the convolution dg Lie algebra

$\Pi_{k\in\mathbb{N}}Hom_{\Sigma_{k}}(\mathcal{E}_{n}^{i}(k),\Omega e_{n}^{i}(k))$

where $\Omega e_{n}^{i}$ is the minimal model of $e_{n}$.

Proof:

Since $\mathcal{E}_{n}$ is an $E_{n}$-operad, by the definition of $E_{n}$-operads there is a zig-zag of quasi-isomorphisms of dg-operads

$\mathcal{E}_{n}\overset{\simeq}{\longleftarrow}\bullet\overset{\simeq}{\longrightarrow}\cdots\overset{\simeq}{\longleftarrow}\bullet\overset{\simeq}{\longrightarrow}e_{n}$

where we consider $e_{n}$ as a differential graded operad with trivial differential in each arity. Now since in both cases ($\mathcal{E}_{n}$ as well as $e_{n}$), the appropriate Koszul dual cooperads $\mathcal{E}_{n}^{i}$ and $e_{n}^{i}$ are the linear duals "up to tensoring with appropriate shifting cooperads", this implies the existence of the following diagram of dg-cooperad quasi-isomorphisms:

$\mathcal{E}_{n}^{i}\overset{\simeq}{\longrightarrow}\bullet\overset{\simeq}{\longleftarrow}\cdots\overset{\simeq}{\longrightarrow}\bullet\overset{\simeq}{\longleftarrow}e_{n}^{i}$

since the linear dual of a quasi-isomorphism is a quasi-isomorphism. Now if we change the category of differential graded cooperads with morphisms of differential graded cooperads into the category of dg cooperads with infinity morphisms of dg cooperads (Such an infinity morphism $F_{\infty}:\mathcal{C}_{1}\rightsquigarrow\mathcal{C}_{2}$ is defined as (or equivalent to ) a morphism of dg operads $\Omega F_{\infty}:\Omega\mathcal{C}_{1}\to\Omega\mathcal{C}_{2}$ ) then any quasi-isomorphism has an actual inverse in terms of these infinity morphisms (To emphasis these different kind of maps, I write $\rightsquigarrow$ for them). Therefore in this other category, there exist the following diagram of dg-cooperad infinity-isomorphisms

$\mathcal{E}_{n}^{i}\overset{\simeq}{\rightsquigarrow}\bullet\overset{\simeq}{\rightsquigarrow}\cdots\overset{\simeq}{\rightsquigarrow}\bullet\overset{\simeq}{\rightsquigarrow}e_{n}^{i}$

and by composition, we get a single infinity isomorphism of dg-cooperads $\mathcal{E}_{n}^{i}\rightsquigarrow e_{n}^{i}$. By definition of these infinity morphisms, this is equivalent to the existence of an ordinary isomorphism of dg-operads

$\Omega\mathcal{E}_{n}^{i}\to\Omega e_{n}^{i}$

which in turn is equivalent to the existence of a solution to the Maurer Cartan equation in $\Pi_{k\in\mathbb{N}}Hom_{\Sigma_{k}}(\mathcal{E}_{n}^{i}(k),\Omega e_{n}^{i}(k))$.

q.e.d.

Second question: The proof relays on the transition from ordinary morphisms of dg-cooperads to the $\infty$-morphisms of dg-cooperads. Is this the transition to the derived category of dg-cooperads?