[proofplan] We work in a local exponential chart near the identity and write products of exponentials using the Baker--Campbell--Hausdorff expansion. First we expand $\exp X\exp Y$ to second order, then multiply successively by $\exp(-X)$ and $\exp(-Y)$, discarding only terms whose total degree is at least $3$. The linear terms cancel because the commutator word has zero total exponent in both $X$ and $Y$, and the unique surviving quadratic term is the Lie bracket $[X,Y]$. [/proofplan] [step:Choose a local BCH chart and fix the meaning of the remainder] Let \begin{align*} C:W\subset \mathfrak g\times \mathfrak g\to \mathfrak g \end{align*} denote the local Baker--Campbell--Hausdorff map, defined on a neighbourhood $W$ of $(0,0)$, so that \begin{align*} \exp C(A,B)=\exp A\exp B \end{align*} whenever $(A,B)\in W$ and the products remain in the chosen exponential neighbourhood. By the Baker--Campbell--Hausdorff expansion to degree three [citetheorem:8796], after shrinking $W$ if necessary, \begin{align*} C(A,B)=A+B+\frac{1}{2}[A,B]+O_3(A,B), \end{align*} where $O_3(A,B)$ denotes a smooth $\mathfrak g$-valued remainder whose Taylor expansion at $(0,0)$ has no terms of total degree less than $3$. Choose a symmetric neighbourhood $U\subset \mathfrak g$ of $0$ small enough that all BCH expressions \begin{align*} C(X,Y),\qquad C(C(X,Y),-X),\qquad C(C(C(X,Y),-X),-Y) \end{align*} are defined for $X,Y\in U$. For two smooth $\mathfrak g$-valued expressions $P(X,Y)$ and $Q(X,Y)$, write \begin{align*} P(X,Y)\equiv Q(X,Y)\pmod{O_3(X,Y)} \end{align*} to mean that $P-Q$ has Taylor expansion at $(0,0)$ with no homogeneous terms of total degree less than $3$. We will also use the following consequence of Taylor expansion under composition: if $E(A,B)=O_3(A,B)$ and $A(X,Y),B(X,Y)$ vanish at $(0,0)$, then $E(A(X,Y),B(X,Y))=O_3(X,Y)$. [guided] The proof is local, so the first task is to place every product inside one exponential coordinate chart. Let \begin{align*} C:W\subset \mathfrak g\times \mathfrak g\to \mathfrak g \end{align*} be the local Baker--Campbell--Hausdorff map. Its defining property is \begin{align*} \exp C(A,B)=\exp A\exp B \end{align*} for pairs $(A,B)$ sufficiently close to $(0,0)$. This is exactly the tool needed because the group commutator is a product of four exponentials, and BCH allows us to rewrite that product as one exponential after multiplying factors one at a time. By the Baker--Campbell--Hausdorff expansion to degree three [citetheorem:8796], the logarithm of a product of two nearby exponentials satisfies \begin{align*} C(A,B)=A+B+\frac{1}{2}[A,B]+O_3(A,B). \end{align*} Here $O_3(A,B)$ is not a scalar bound but a Lie-algebra-valued smooth remainder. Saying that it has total degree at least $3$ means its Taylor expansion at $(0,0)$ contains no constant, linear, or quadratic homogeneous terms. We now choose a symmetric neighbourhood $U\subset \mathfrak g$ of $0$ small enough that each intermediate BCH expression is defined: \begin{align*} C(X,Y),\qquad C(C(X,Y),-X),\qquad C(C(C(X,Y),-X),-Y). \end{align*} This shrinking is legitimate because each expression is built from smooth maps defined near $0$. Finally, we write \begin{align*} P(X,Y)\equiv Q(X,Y)\pmod{O_3(X,Y)} \end{align*} when $P-Q$ has no Taylor terms of total degree less than $3$. This notation records precisely which terms affect the desired second-order expansion. The notation is stable under the substitutions used below: if a BCH remainder is $O_3(A,B)$ and the substituted expressions $A(X,Y)$ and $B(X,Y)$ vanish at $(0,0)$, then the composite remainder is $O_3(X,Y)$ by Taylor expansion under smooth composition. [/guided] [/step] [step:Expand the first product $\exp X\exp Y$ through degree two] Define \begin{align*} Z_1(X,Y):=C(X,Y). \end{align*} Using the BCH expansion with $A=X$ and $B=Y$, we obtain \begin{align*} Z_1(X,Y)\equiv X+Y+\frac{1}{2}[X,Y]\pmod{O_3(X,Y)}. \end{align*} Thus \begin{align*} \exp X\exp Y=\exp Z_1(X,Y). \end{align*} [/step] [step:Multiply by $\exp(-X)$ and keep all quadratic terms] Define \begin{align*} Z_2(X,Y):=C(Z_1(X,Y),-X). \end{align*} Then \begin{align*} \exp Z_2(X,Y)=\exp X\exp Y\exp(-X). \end{align*} Applying BCH to $C(Z_1,-X)$ gives \begin{align*} Z_2\equiv Z_1-X+\frac{1}{2}[Z_1,-X]\pmod{O_3(X,Y)}. \end{align*} In the commutator term only the degree-one part $X+Y$ of $Z_1$ can contribute to degree two, since bracketing the quadratic term $\frac{1}{2}[X,Y]$ with $-X$ gives degree three. Hence \begin{align*} [Z_1,-X]\equiv [X+Y,-X]\pmod{O_3(X,Y)}. \end{align*} Using bilinearity and antisymmetry of the Lie bracket, \begin{align*} [X+Y,-X]=-[X,X]-[Y,X]=[X,Y]. \end{align*} Therefore \begin{align*} Z_2\equiv Y+\frac{1}{2}[X,Y]+\frac{1}{2}[X,Y]\pmod{O_3(X,Y)}. \end{align*} Thus \begin{align*} Z_2\equiv Y+[X,Y]\pmod{O_3(X,Y)}. \end{align*} [guided] We now multiply the first two factors by $\exp(-X)$. Define \begin{align*} Z_2(X,Y):=C(Z_1(X,Y),-X). \end{align*} By the defining property of the BCH map, \begin{align*} \exp Z_2(X,Y)=\exp Z_1(X,Y)\exp(-X)=\exp X\exp Y\exp(-X). \end{align*} The BCH formula gives \begin{align*} Z_2\equiv Z_1-X+\frac{1}{2}[Z_1,-X]\pmod{O_3(X,Y)}. \end{align*} We must compute each part through total degree two. From the previous step, \begin{align*} Z_1\equiv X+Y+\frac{1}{2}[X,Y]\pmod{O_3(X,Y)}. \end{align*} The linear part of $Z_1-X$ is $Y$, and its quadratic part is $\frac{1}{2}[X,Y]$. For the bracket $[Z_1,-X]$, only the linear part of $Z_1$ matters at quadratic order. The term $\frac{1}{2}[X,Y]$ already has total degree two, and bracketing it with $-X$ raises the total degree to three. Hence \begin{align*} [Z_1,-X]\equiv [X+Y,-X]\pmod{O_3(X,Y)}. \end{align*} Bilinearity gives \begin{align*} [X+Y,-X]=[X,-X]+[Y,-X]. \end{align*} Since $[X,X]=0$ by antisymmetry, the first term vanishes. Also $[Y,-X]=-[Y,X]=[X,Y]$. Thus \begin{align*} [Z_1,-X]\equiv [X,Y]\pmod{O_3(X,Y)}. \end{align*} Substituting this into the BCH expansion gives \begin{align*} Z_2\equiv Y+\frac{1}{2}[X,Y]+\frac{1}{2}[X,Y]\pmod{O_3(X,Y)}. \end{align*} Therefore \begin{align*} Z_2\equiv Y+[X,Y]\pmod{O_3(X,Y)}. \end{align*} This is the first cancellation: the $X$ term has disappeared after multiplying by $\exp(-X)$. [/guided] [/step] [step:Multiply by $\exp(-Y)$ and identify the commutator term] Define \begin{align*} Z_3(X,Y):=C(Z_2(X,Y),-Y). \end{align*} Then \begin{align*} \exp Z_3(X,Y)=\exp X\exp Y\exp(-X)\exp(-Y). \end{align*} Using BCH once more, \begin{align*} Z_3\equiv Z_2-Y+\frac{1}{2}[Z_2,-Y]\pmod{O_3(X,Y)}. \end{align*} From the preceding step, \begin{align*} Z_2-Y\equiv [X,Y]\pmod{O_3(X,Y)}. \end{align*} In the bracket term, the degree-one part of $Z_2$ is $Y$, so \begin{align*} [Z_2,-Y]\equiv [Y,-Y]\pmod{O_3(X,Y)}. \end{align*} By antisymmetry, $[Y,-Y]=0$. Therefore \begin{align*} Z_3\equiv [X,Y]\pmod{O_3(X,Y)}. \end{align*} Equivalently, there is a smooth map $R:U\times U\to\mathfrak g$ whose Taylor expansion at $(0,0)$ has no homogeneous terms of total degree less than $3$ such that \begin{align*} Z_3(X,Y)=[X,Y]+R(X,Y). \end{align*} [guided] We now multiply by the final factor $\exp(-Y)$. Define \begin{align*} Z_3(X,Y):=C(Z_2(X,Y),-Y). \end{align*} The defining property of the BCH map gives \begin{align*} \exp Z_3(X,Y)=\exp Z_2(X,Y)\exp(-Y)=\exp X\exp Y\exp(-X)\exp(-Y). \end{align*} Using the BCH expansion with $A=Z_2(X,Y)$ and $B=-Y$, and using the composition stability of the $O_3$ remainder because $Z_2(0,0)=0$, we get \begin{align*} Z_3\equiv Z_2-Y+\frac{1}{2}[Z_2,-Y]\pmod{O_3(X,Y)}. \end{align*} From the previous step, \begin{align*} Z_2\equiv Y+[X,Y]\pmod{O_3(X,Y)}. \end{align*} Therefore \begin{align*} Z_2-Y\equiv [X,Y]\pmod{O_3(X,Y)}. \end{align*} For the bracket term, only the degree-one part of $Z_2$ can affect degree two. That degree-one part is $Y$, while $[X,Y]$ already has total degree two and would become degree three after bracketing with $-Y$. Hence \begin{align*} [Z_2,-Y]\equiv [Y,-Y]\pmod{O_3(X,Y)}. \end{align*} By antisymmetry of the Lie bracket, $[Y,-Y]=0$. Substituting this into the BCH expansion gives \begin{align*} Z_3\equiv [X,Y]\pmod{O_3(X,Y)}. \end{align*} Thus there is a smooth map $R:U\times U\to\mathfrak g$ with no Taylor terms of total degree less than $3$ such that \begin{align*} Z_3(X,Y)=[X,Y]+R(X,Y). \end{align*} [/guided] [/step] [step:Return from logarithms to the group commutator] By the definition of $Z_3$ and the choice of $U$, \begin{align*} \exp X\exp Y\exp(-X)\exp(-Y)=\exp Z_3(X,Y). \end{align*} The previous step gives \begin{align*} Z_3(X,Y)=[X,Y]+R(X,Y), \end{align*} where $R(X,Y)=O_3(X,Y)$ in the precise Taylor sense fixed above. Hence \begin{align*} \exp X\exp Y\exp(-X)\exp(-Y)=\exp\bigl([X,Y]+O_3(X,Y)\bigr). \end{align*} This is the claimed group commutator expansion for all $X,Y$ in a sufficiently small neighbourhood of $0\in\mathfrak g$. [guided] The element $Z_3(X,Y)$ was defined as the BCH logarithm of the full commutator word. By construction and by the choice of $U$, \begin{align*} \exp X\exp Y\exp(-X)\exp(-Y)=\exp Z_3(X,Y). \end{align*} The preceding computation proved that \begin{align*} Z_3(X,Y)=[X,Y]+R(X,Y), \end{align*} where $R:U\times U\to\mathfrak g$ is smooth and its Taylor expansion at $(0,0)$ contains no homogeneous terms of total degree less than $3$. Substituting this logarithm back into the exponential gives \begin{align*} \exp X\exp Y\exp(-X)\exp(-Y)=\exp\bigl([X,Y]+R(X,Y)\bigr). \end{align*} This is precisely the notation \begin{align*} \exp X\exp Y\exp(-X)\exp(-Y)=\exp\bigl([X,Y]+O_3(X,Y)\bigr), \end{align*} with $O_3(X,Y)$ understood as the third-order Lie-algebra-valued local remainder $R(X,Y)$. [/guided] [/step]