Commutator relations in associated algebra. Consider the free associated algebra over some field $k$
$$k\langle x_1,\cdots,x_n\rangle.$$
Order the generators $x_1<\cdots<x_m$.
I can define a complete bracket of an ordered monomial $x_{i_1}\cdots x_{i_k}$ with $i_1\leq\cdots\leq i_k$ by
$$[x_{i_1}\cdots x_{i_k}]:=[\cdots[x_{i_1},x_{i_2}],x_{i_3}],\cdots],x_{i_k}]$$
where $[-,-]$ is the binary Lie bracket. If there is only one $x_i$, then we define $[x_i]:=x_i$.
Here are some observations

*

*$2x_1x_2=[x_1x_2]+\big(x_2[x_1]+x_1[x_2]\big)$

*$3x_1x_2x_3=[x_1x_2x_3]+\big(x_1[x_2x_3]+x_2[x_1x_3]+x_3[x_1x_2]\big)+\big(x_1x_2[x_3]+x_1x_3[x_2]+x_2x_3[x_1]\big)$
The obvious guess would be
$$n\;x_1\cdots x_n=\sum_{m=1}^n\sum_{i_1<\cdots<i_m}(\cdots\hat x_{i_1}\cdots\hat x_{i_m}\cdots)[x_{i_1}\cdots x_{i_m}]. \quad (*)$$
This looks very symmetric and I tend to believe it, and I also want to believe there is a ''symmetric'' proof.
One motivation for this definition comes from the notion of a universal enveloping algebra $U(\mathfrak g)$ of a Lie algebra $\mathfrak g$. By the Poincaré-Birkhoff-Witt theorem, if we choose an ordered basis $\xi_1<\cdots<\xi_n$ of $\mathfrak g$, then $\xi_1^{k_1}\cdots\xi_n^{k_n}$ with $(k_1,\cdots,k_n)\in\mathbb N^n$ form a basis of $U(\mathfrak g)$. The complete bracket of such a base vector is always in $\mathfrak g$.
I want to ask:

*

*Is there a name for what I call complete bracket? I think people should have considered it.

*Of course a proof of $(*)$, or a counterexample.

Any comments are welcome.
 A: It turns out the proof of the formula is not difficult by induction on $n$.
I would like to post and prove a more flexible formula
$$(w_1+\cdots+w_n)x_1\cdots x_n=\sum_{m=1}^n\sum_{i_1<\cdots<i_m}w_{i_1}(\cdots\hat x_{i_1}\cdots\hat x_{i_m}\cdots)[x_{i_1}\cdots x_{i_m}]\quad (**)$$
and we recover the equation in the question by letting $w_1=\cdots=w_n=1$.
The formula $(**)$ for $n=2$ is the easy-to-check identity
$$(w_1+w_2)x_1x_2=w_1x_2[x_1]+w_2x_1[x_2]+w_1[x_1x_2]. $$
To make equations look more compact, I introduce some notations:

*

*$[n]:=\{1,\cdots,n\}$;

*for a nonempty subset $S\subset[n]$, it is $S=\{i_1<\cdots<i_s\}$, and denote $x^S:=x_{i_1}\cdots x_{i_s}$, and $[x^S]:=[x_{i_1}\cdots x_{i_s}]$.

With above notations, the formula we will prove is
\begin{equation}
 (w_1+\cdots+w_n)x^{[n]}=\sum_{\emptyset\ne S\subset[n]}w_{\min(S)}x^{[n]\setminus S}[x^S]. 
\end{equation}
Assume we have shown the equation for $n$. For $n+1$, we use variables $y_1,\cdots,y_{n+1}$, and let $x$ be the truncation $y_{\leq n}$, i.e. $(x_1,\cdots,x_n)=(y_1,\cdots,y_n)$. We have
\begin{equation}
 \begin{split}
  &\sum_{\emptyset\ne S\subset[n+1]}w_{\min(S)}y^{[n+1]\setminus S}[y^S]\\
  =&\sum_{\substack{S\subset[n]\\S\ne\emptyset}}+\sum_{S=\{n+1\}}+\sum_{\substack{S=\{n+1\}\sqcup S'\\S'\subset [n]\\S'\ne\emptyset}}\\
  =&\sum_{\substack{S\subset[n]\\S\ne\emptyset}}w_{\min(S)}x^{[n]\setminus S}y_{n+1}[x^S]+w_{n+1}y^{[n+1]}+\sum_{\substack{S'\subset[n]\\S'\ne\emptyset}}w_{\min(S')}x^{[n]\setminus S'}\big[[x^{S'}],y_{n+1}\big]\\
  =&\sum_{\substack{S\subset[n]\\S\ne\emptyset}}w_{\min(S)}x^{[n]\setminus S}[x^S]y_{n+1}+w_{n+1}y^{[n+1]}\\
  =&(w_1+\cdots+w_n)x^{[n]}y_{n+1}+w_{n+1}y^{[n+1]}\\
  =&(w_1+\cdots+w_{n+1})y^{[n+1]}
 \end{split}
\end{equation}
