[proofplan] Choose the small neighbourhoods so that $\exp$ is a logarithm chart and the path $\exp X\exp(tY)$ stays inside that chart for $0\le t\le 1$. The identity $\exp Z(t)=\exp X\exp(tY)$ is then differentiated as an equality of matrix-valued smooth paths. After left-trivialising the tangent vector, the right-hand side becomes $Y$, while the left-hand side is the left-trivialised differential of the exponential map at $Z(t)$. The standard formula for this differential gives an operator equation, and inverting the convergent [power series](/page/Power%20Series) near $0$ gives the claimed differential equation. [/proofplan] [step:Choose a logarithm chart containing the whole path] By [Exponential Is A Local Diffeomorphism][citetheorem:8791], there are neighbourhoods $U\subset\mathfrak g$ of $0$ and $V\subset G$ of the identity matrix $I\in G$ such that \begin{align*} \exp|_U:U\to V \end{align*} is a diffeomorphism with inverse denoted \begin{align*} \log:V\to U. \end{align*} Since multiplication \begin{align*} m:G\times G\to G,\qquad (g,h)\mapsto gh \end{align*} and the exponential map are smooth, the map \begin{align*} F:\mathfrak g\times\mathfrak g\times[0,1]\to G,\qquad (A,B,t)\mapsto \exp A\exp(tB) \end{align*} is continuous. Also $F(0,0,t)=I$ for every $t\in[0,1]$. For each $t_0\in[0,1]$, continuity of $F$ at $(0,0,t_0)$ gives neighbourhoods $P_{t_0},Q_{t_0}\subset\mathfrak g$ of $0$ and an open interval $J_{t_0}\subset\mathbb R$ containing $t_0$ such that \begin{align*} F(P_{t_0}\times Q_{t_0}\times(J_{t_0}\cap[0,1]))\subset V. \end{align*} The intervals $J_{t_0}\cap[0,1]$ cover $[0,1]$, so compactness gives finitely many points $t_1,\dots,t_N\in[0,1]$ whose intervals cover $[0,1]$. Define \begin{align*} U_X:=\bigcap_{j=1}^{N}P_{t_j},\qquad U_Y:=\bigcap_{j=1}^{N}Q_{t_j}. \end{align*} Then $U_X$ and $U_Y$ are neighbourhoods of $0$ in $\mathfrak g$, and \begin{align*} F(U_X\times U_Y\times[0,1])\subset V. \end{align*} Fix $X\in U_X$ and $Y\in U_Y$. Then the map \begin{align*} Z:[0,1]\to\mathfrak g,\qquad t\mapsto \log(\exp X\exp(tY)) \end{align*} is smooth, because it is the composition of the smooth path $t\mapsto\exp X\exp(tY)$ with the smooth chart inverse $\log:V\to U$. [/step] [step:Differentiate the defining identity and left-trivialise it] For every $t\in[0,1]$, the definition of $Z$ gives \begin{align*} \exp Z(t)=\exp X\exp(tY). \end{align*} Differentiate both sides with respect to $t$. On the left, the chain rule for the smooth map $\exp:\mathfrak g\to G\subset M(n,\mathbb C)$ gives \begin{align*} \frac{d}{dt}\exp Z(t)=(d\exp)_{Z(t)}(Z'(t)). \end{align*} On the right, $\exp X$ is constant in $t$, and the one-parameter subgroup identity gives \begin{align*} \frac{d}{dt}\exp(tY)=\exp(tY)Y. \end{align*} Therefore \begin{align*} (d\exp)_{Z(t)}(Z'(t))=\exp X\exp(tY)Y. \end{align*} Using $\exp Z(t)=\exp X\exp(tY)$, this becomes \begin{align*} (d\exp)_{Z(t)}(Z'(t))=\exp Z(t)Y. \end{align*} Multiplying on the left by $\exp(-Z(t))$ gives the left-trivialised identity \begin{align*} \exp(-Z(t))(d\exp)_{Z(t)}(Z'(t))=Y. \end{align*} [guided] The point of this step is to turn an equality of tangent vectors in the matrix group into an equality inside the fixed [vector space](/page/Vector%20Space) $\mathfrak g$. The defining identity is \begin{align*} \exp Z(t)=\exp X\exp(tY). \end{align*} Both sides are smooth paths in $G\subset M(n,\mathbb C)$, so we may differentiate them as matrix-valued paths. For the left side, the chain rule applied to the smooth map \begin{align*} \exp:\mathfrak g\to G \end{align*} and the smooth path \begin{align*} Z:[0,1]\to\mathfrak g \end{align*} gives \begin{align*} \frac{d}{dt}\exp Z(t)=(d\exp)_{Z(t)}(Z'(t)). \end{align*} For the right side, the factor $\exp X$ is independent of $t$. Since $Y$ commutes with every power of $tY$, differentiating the matrix exponential series gives \begin{align*} \frac{d}{dt}\exp(tY)=\exp(tY)Y. \end{align*} Thus \begin{align*} (d\exp)_{Z(t)}(Z'(t))=\exp X\exp(tY)Y. \end{align*} Now substitute the original identity $\exp X\exp(tY)=\exp Z(t)$: \begin{align*} (d\exp)_{Z(t)}(Z'(t))=\exp Z(t)Y. \end{align*} The derivative on the left is a tangent vector at $\exp Z(t)$. Left multiplication by $\exp(-Z(t))$ transports this tangent vector back to the tangent space at the identity, which is $\mathfrak g$. Performing this multiplication gives \begin{align*} \exp(-Z(t))(d\exp)_{Z(t)}(Z'(t))=Y. \end{align*} This is the useful form because the differential of $\exp$ has a standard power-series expression after left trivialisation. [/guided] [/step] [step:Express the left-trivialised differential of the exponential] For $g\in G$, let $R_g:G\to G$ denote the right-translation map $h\mapsto hg$. By [Differential Of The Exponential][citetheorem:8834], for every $A,V\in\mathfrak g$, \begin{align*} (d\exp)_A(V)=(dR_{\exp A})_I\left(\sum_{k=0}^{\infty}\frac{(\operatorname{ad}_A)^k(V)}{(k+1)!}\right). \end{align*} Equivalently, after left translation back to the identity, this formula is \begin{align*} \exp(-A)(d\exp)_A(V)=\sum_{k=0}^{\infty}\frac{(-1)^k(\operatorname{ad}_A)^k(V)}{(k+1)!}. \end{align*} The series on the right is exactly \begin{align*} \frac{1-e^{-\operatorname{ad}_A}}{\operatorname{ad}_A}(V). \end{align*} Applying this identity with $A=Z(t)$ and $V=Z'(t)$ gives \begin{align*} \exp(-Z(t))(d\exp)_{Z(t)}(Z'(t))=\frac{1-e^{-\operatorname{ad}_{Z(t)}}}{\operatorname{ad}_{Z(t)}}(Z'(t)). \end{align*} Combining this with the left-trivialised identity from the previous step yields \begin{align*} \frac{1-e^{-\operatorname{ad}_{Z(t)}}}{\operatorname{ad}_{Z(t)}}(Z'(t))=Y. \end{align*} [/step] [step:Invert the operator power series near zero] Define the scalar [holomorphic function](/page/Holomorphic%20Function) \begin{align*} \phi:B(0,2\pi)\to\mathbb C,\qquad w\mapsto \sum_{k=0}^{\infty}\frac{(-1)^k w^k}{(k+1)!}. \end{align*} For $w\ne0$ this equals $(1-e^{-w})/w$, and the series gives $\phi(0)=1$. Choose an open neighbourhood $W\subset B(0,2\pi)$ of $0$ on which $\phi$ has no zero, and define \begin{align*} \psi:W\to\mathbb C,\qquad w\mapsto \frac{1}{\phi(w)}. \end{align*} Thus $\psi(w)=w/(1-e^{-w})$ for $w\ne0$. Choose $r>0$ such that the closed disk $\{w\in\mathbb C:|w|\le r\}$ is contained in $W$ and the power series for $\psi$ converges on $B(0,r)$. Fix an operator norm on $\mathcal L(\mathfrak g,\mathfrak g)$. Since the maps $(X,Y,t)\mapsto Z(t)=\log(\exp X\exp(tY))$ and $A\mapsto\operatorname{ad}_A$ are continuous, and since $\operatorname{ad}_{Z(t)}=0$ when $X=Y=0$, compactness of $[0,1]$ allows us, after shrinking $U_X$ and $U_Y$, to assume that \begin{align*} \|\operatorname{ad}_{Z(t)}\|_{\mathcal L(\mathfrak g,\mathfrak g)}<r \end{align*} for every $t\in[0,1]$. Hence the operator series $\psi(\operatorname{ad}_{Z(t)})$ converges and is the inverse of $\phi(\operatorname{ad}_{Z(t)})$. Applying this inverse to \begin{align*} \phi(\operatorname{ad}_{Z(t)})(Z'(t))=Y \end{align*} gives \begin{align*} Z'(t)=\psi(\operatorname{ad}_{Z(t)})(Y). \end{align*} By the definition of $\psi$, this is \begin{align*} \frac{dZ}{dt}(t)=\frac{\operatorname{ad}_{Z(t)}}{1-e^{-\operatorname{ad}_{Z(t)}}}(Y). \end{align*} [guided] The previous step produced the operator equation \begin{align*} \phi(\operatorname{ad}_{Z(t)})(Z'(t))=Y, \end{align*} where the scalar holomorphic function \begin{align*} \phi:B(0,2\pi)\to\mathbb C,\qquad w\mapsto \sum_{k=0}^{\infty}\frac{(-1)^k w^k}{(k+1)!} \end{align*} satisfies $\phi(w)=(1-e^{-w})/w$ for $w\ne0$ and $\phi(0)=1$. Because $\phi$ is holomorphic and nonzero at $0$, there is an open neighbourhood $W\subset B(0,2\pi)$ of $0$ on which $\phi$ has no zero. On this neighbourhood we define the reciprocal holomorphic function \begin{align*} \psi:W\to\mathbb C,\qquad w\mapsto \frac{1}{\phi(w)}. \end{align*} Thus $\psi(w)=w/(1-e^{-w})$ for $w\ne0$. We must justify that this scalar reciprocal may be applied to the operator $\operatorname{ad}_{Z(t)}$ uniformly for all $t\in[0,1]$. Choose $r>0$ such that the closed disk $\{w\in\mathbb C:|w|\le r\}$ is contained in $W$ and the power series for $\psi$ converges on $B(0,r)$. Fix an operator norm on $\mathcal L(\mathfrak g,\mathfrak g)$. The map $(X,Y,t)\mapsto Z(t)=\log(\exp X\exp(tY))$ is continuous wherever the logarithm chart is defined, and the [linear map](/page/Linear%20Map) $A\mapsto\operatorname{ad}_A$ from $\mathfrak g$ to $\mathcal L(\mathfrak g,\mathfrak g)$ is continuous because $\mathfrak g$ is finite-dimensional. At $(X,Y)=(0,0)$ we have $Z(t)=0$ and hence $\operatorname{ad}_{Z(t)}=0$ for every $t\in[0,1]$. Since $[0,1]$ is compact, we may shrink $U_X$ and $U_Y$ so that \begin{align*} \|\operatorname{ad}_{Z(t)}\|_{\mathcal L(\mathfrak g,\mathfrak g)}<r \end{align*} for every $t\in[0,1]$. With this shrinking in force, the operator series $\psi(\operatorname{ad}_{Z(t)})$ converges. Since $\psi\phi=1$ as scalar power series on the convergence neighbourhood, the corresponding operator power series satisfy \begin{align*} \psi(\operatorname{ad}_{Z(t)})\phi(\operatorname{ad}_{Z(t)})=\operatorname{id}_{\mathfrak g}. \end{align*} Applying this inverse operator to \begin{align*} \phi(\operatorname{ad}_{Z(t)})(Z'(t))=Y \end{align*} gives \begin{align*} Z'(t)=\psi(\operatorname{ad}_{Z(t)})(Y). \end{align*} Substituting the definition of $\psi$ yields \begin{align*} \frac{dZ}{dt}(t)=\frac{\operatorname{ad}_{Z(t)}}{1-e^{-\operatorname{ad}_{Z(t)}}}(Y). \end{align*} [/guided] This proves the asserted differential equation for every $t\in[0,1]$. [/step]