# $L\in NC^1$ iff there exists a sequence of poly sized formulas that decides $L$

Prove that $L\in NC^1$ iff there exists a sequence of poly sized formulas that decides $L$.

I managed to prove the $(\impliedby)$ and I want to prove $(\implies)$.

I feel that we need to take the boolean circuit and duplicate the sub-circuits of $fan-out\gt 1$ into exact circuits but with $fan-out = 1$. I fail to argue why the resulting tree is of polynomial size and not of exponential one.

If a function is computed by a fan-in 2 circuit of size $S$ and depth $D$, then it is computed by a formula of size $2^D S$.
If $L$ is in NC1 then its $n$-bit fragments have circuits of size $n^{O(1)}$ and depth $O(\log n)$. The claim shows that there are equivalent formulas of size $n^{O(1)} 2^{O(\log n)} = n^{O(1)}$.