[proofplan]
The defining equation for the symplectic group is $A^\top J A=J$. We first differentiate this identity along a smooth path through the identity, which gives the infinitesimal condition $B^\top J+JB=0$. We then rewrite this condition using $J^\top=-J$ to obtain the equivalent symmetry of $JB$. For the converse, we use the matrix exponential path $A(t)=\exp(tB)$ and prove that $A(t)^\top J A(t)$ has zero derivative, hence is constantly equal to $J$.
[/proofplan]
[step:Differentiate the symplectic identity at the identity]
Since $A(t)\in Sp(2n,\mathbb R)$ for every $t\in(-\varepsilon,\varepsilon)$, the defining identity gives
\begin{align*}
A(t)^\top J A(t)=J
\end{align*}
for every $t\in(-\varepsilon,\varepsilon)$. Define
\begin{align*}
F:(-\varepsilon,\varepsilon)&\to\mathbb R^{2n\times 2n}, & F(t)&=A(t)^\top J A(t).
\end{align*}
The path $F$ is smooth because matrix multiplication and transpose are smooth polynomial operations in the entries. Since $F(t)$ is constant and equal to $J$, we have $F'(0)=0$.
Using the product rule for matrix-valued functions,
\begin{align*}
F'(0)=A'(0)^\top J A(0)+A(0)^\top J A'(0).
\end{align*}
Substituting $A(0)=I_{2n}$ and $A'(0)=B$ gives
\begin{align*}
0=F'(0)=B^\top J+JB.
\end{align*}
Thus every initial velocity of a smooth path in $Sp(2n,\mathbb R)$ through $I_{2n}$ satisfies the infinitesimal symplectic condition.
[guided]
The only input from the definition of $Sp(2n,\mathbb R)$ is that every matrix on the path preserves $J$. Thus, for each $t\in(-\varepsilon,\varepsilon)$,
\begin{align*}
A(t)^\top J A(t)=J.
\end{align*}
To extract the infinitesimal condition at $t=0$, define the matrix-valued function
\begin{align*}
F:(-\varepsilon,\varepsilon)&\to\mathbb R^{2n\times 2n}, & F(t)&=A(t)^\top J A(t).
\end{align*}
Because $A$ is smooth and transpose and matrix multiplication are smooth operations on matrix entries, $F$ is smooth. The equation above says that $F$ is the constant function with value $J$, so its derivative at $0$ is the zero matrix:
\begin{align*}
F'(0)=0.
\end{align*}
Now compute $F'(0)$ carefully. The matrix $J$ is constant in $t$, so the product rule gives
\begin{align*}
F'(0)=A'(0)^\top J A(0)+A(0)^\top J A'(0).
\end{align*}
The hypotheses give $A(0)=I_{2n}$ and define
\begin{align*}
B=A'(0).
\end{align*}
Substituting these two identities into the derivative formula yields
\begin{align*}
0=F'(0)=B^\top J+JB.
\end{align*}
This is exactly the claimed infinitesimal constraint on the tangent vector $B$.
[/guided]
[/step]
[step:Rewrite the infinitesimal condition as symmetry of $JB$]
Since $J^\top=-J$, we have
\begin{align*}
(JB)^\top=B^\top J^\top=-B^\top J.
\end{align*}
If $B^\top J+JB=0$, then $B^\top J=-JB$, so
\begin{align*}
(JB)^\top=JB.
\end{align*}
Thus $JB$ is symmetric.
Conversely, if $JB$ is symmetric, then
\begin{align*}
JB=(JB)^\top=-B^\top J.
\end{align*}
Rearranging gives
\begin{align*}
B^\top J+JB=0.
\end{align*}
Therefore the two conditions are equivalent.
[/step]
[step:Construct a symplectic path from an infinitesimal symplectic matrix]
Assume now that $B\in\mathbb R^{2n\times 2n}$ satisfies
\begin{align*}
B^\top J+JB=0.
\end{align*}
Define
\begin{align*}
A:\mathbb R&\to GL(2n,\mathbb R), & A(t)&=\exp(tB).
\end{align*}
The matrix exponential is smooth, $A(0)=\exp(0)=I_{2n}$, and
\begin{align*}
A'(t)=B\exp(tB)=BA(t).
\end{align*}
In particular,
\begin{align*}
A'(0)=B.
\end{align*}
Define
\begin{align*}
G:\mathbb R&\to\mathbb R^{2n\times 2n}, & G(t)&=A(t)^\top J A(t).
\end{align*}
Using the product rule and $A'(t)=BA(t)$, we obtain
\begin{align*}
G'(t)=A'(t)^\top J A(t)+A(t)^\top J A'(t).
\end{align*}
Hence
\begin{align*}
G'(t)=A(t)^\top B^\top J A(t)+A(t)^\top J B A(t).
\end{align*}
Factoring out $A(t)^\top$ on the left and $A(t)$ on the right gives
\begin{align*}
G'(t)=A(t)^\top(B^\top J+JB)A(t).
\end{align*}
By the assumed infinitesimal condition, this is the zero matrix for every $t\in\mathbb R$. Therefore $G$ is constant. Since
\begin{align*}
G(0)=I_{2n}^\top J I_{2n}=J,
\end{align*}
we have
\begin{align*}
A(t)^\top J A(t)=J
\end{align*}
for every $t\in\mathbb R$. Thus $A(t)\in Sp(2n,\mathbb R)$ for every $t$, and $A$ is the required smooth path with initial velocity $B$.
[/step]
