[proofplan]
We prove the identity for the tautological one-forms by evaluating both sides at an arbitrary covector $\alpha\in T^*Q'$ and an arbitrary tangent vector $v\in T_\alpha(T^*Q')$. The definition of the tautological form reduces the calculation to the base projection maps $\tau_Q:T^*Q\to Q$ and $\tau_{Q'}:T^*Q'\to Q'$. Since the cotangent lift covers $f^{-1}$, the projected tangent vector is carried by $d(f^{-1})$, and this cancels against $df$ in the pulled-back covector. The symplectic-form identity then follows from $\omega=-d\lambda$ and the standard commutation of pullback with the [exterior derivative](/theorems/1525).
[/proofplan]
[step:Record the cotangent lift and the projection identity it satisfies]
Let
\begin{align*}
\tau_Q:T^*Q\to Q
\end{align*}
and
\begin{align*}
\tau_{Q'}:T^*Q'\to Q'
\end{align*}
denote the cotangent bundle projections. These projections and the defining formula for the tautological one-forms are part of the theorem statement. By the definition of the contravariant cotangent lift, if $\alpha\in T_{q'}^*Q'$ and $q=f^{-1}(q')$, then
\begin{align*}
T^*f(\alpha)=\alpha\circ df_q\in T_q^*Q.
\end{align*}
Therefore $T^*f$ covers $f^{-1}$, meaning
\begin{align*}
\tau_Q\circ T^*f=f^{-1}\circ\tau_{Q'}.
\end{align*}
Differentiating this identity at $\alpha\in T^*Q'$ gives
\begin{align*}
d(\tau_Q)_{T^*f(\alpha)}\circ d(T^*f)_\alpha=d(f^{-1})_{\tau_{Q'}(\alpha)}\circ d(\tau_{Q'})_\alpha.
\end{align*}
[/step]
[step:Evaluate the pulled-back tautological form on an arbitrary tangent vector]
Fix $\alpha\in T_{q'}^*Q'$ and $v\in T_\alpha(T^*Q')$, and set $q=f^{-1}(q')$. By the definition of pullback of a one-form,
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=(\lambda_Q)_{T^*f(\alpha)}\bigl(d(T^*f)_\alpha(v)\bigr).
\end{align*}
The tautological one-form on $T^*Q$ is defined by
\begin{align*}
(\lambda_Q)_\beta(\xi)=\beta\bigl(d(\tau_Q)_\beta(\xi)\bigr)
\end{align*}
for every $\beta\in T^*Q$ and every $\xi\in T_\beta(T^*Q)$. Applying this with $\beta=T^*f(\alpha)$ and $\xi=d(T^*f)_\alpha(v)$ gives
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=T^*f(\alpha)\bigl(d(\tau_Q)_{T^*f(\alpha)}(d(T^*f)_\alpha(v))\bigr).
\end{align*}
Using the differentiated projection identity from the previous step, this becomes
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=T^*f(\alpha)\bigl(d(f^{-1})_{q'}(d(\tau_{Q'})_\alpha(v))\bigr).
\end{align*}
Since $T^*f(\alpha)=\alpha\circ df_q$, we obtain
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=\alpha\bigl(df_q(d(f^{-1})_{q'}(d(\tau_{Q'})_\alpha(v)))\bigr).
\end{align*}
Because $f$ is a diffeomorphism and $q=f^{-1}(q')$, the linear maps $df_q:T_qQ\to T_{q'}Q'$ and $d(f^{-1})_{q'}:T_{q'}Q'\to T_qQ$ are inverse to each other. Hence
\begin{align*}
df_q\circ d(f^{-1})_{q'}=\operatorname{id}_{T_{q'}Q'}.
\end{align*}
Thus
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=\alpha\bigl(d(\tau_{Q'})_\alpha(v)\bigr).
\end{align*}
By the definition of the tautological one-form on $T^*Q'$,
\begin{align*}
\alpha\bigl(d(\tau_{Q'})_\alpha(v)\bigr)=(\lambda_{Q'})_\alpha(v).
\end{align*}
Therefore
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=(\lambda_{Q'})_\alpha(v).
\end{align*}
[guided]
The goal is to prove equality of two one-forms on $T^*Q'$. A one-form is determined by its value on every tangent vector at every point, so we fix a point $\alpha\in T_{q'}^*Q'$ and a vector $v\in T_\alpha(T^*Q')$. Let $q=f^{-1}(q')$.
By the definition of pullback of a one-form,
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=(\lambda_Q)_{T^*f(\alpha)}\bigl(d(T^*f)_\alpha(v)\bigr).
\end{align*}
Now we use the defining property of the tautological one-form. On a cotangent bundle, the tautological form evaluates a tangent vector by first projecting that tangent vector down to the base and then applying the covector at the point of the cotangent bundle. Thus, for every $\beta\in T^*Q$ and every $\xi\in T_\beta(T^*Q)$,
\begin{align*}
(\lambda_Q)_\beta(\xi)=\beta\bigl(d(\tau_Q)_\beta(\xi)\bigr).
\end{align*}
Applying this formula with $\beta=T^*f(\alpha)$ and $\xi=d(T^*f)_\alpha(v)$ gives
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=T^*f(\alpha)\bigl(d(\tau_Q)_{T^*f(\alpha)}(d(T^*f)_\alpha(v))\bigr).
\end{align*}
The point of introducing the projection maps is that the cotangent lift has a precise base map. Since $T^*f:T^*Q'\to T^*Q$ sends a covector over $q'$ to a covector over $f^{-1}(q')$, it covers $f^{-1}$. In symbols,
\begin{align*}
\tau_Q\circ T^*f=f^{-1}\circ\tau_{Q'}.
\end{align*}
Differentiating this identity at $\alpha$ and applying the resulting linear maps to $v$ gives
\begin{align*}
d(\tau_Q)_{T^*f(\alpha)}(d(T^*f)_\alpha(v))=d(f^{-1})_{q'}(d(\tau_{Q'})_\alpha(v)).
\end{align*}
Substituting this into the previous formula yields
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=T^*f(\alpha)\bigl(d(f^{-1})_{q'}(d(\tau_{Q'})_\alpha(v))\bigr).
\end{align*}
Now we use the definition of the cotangent lift itself. Since $q=f^{-1}(q')$, the covector $T^*f(\alpha)\in T_q^*Q$ is the composite
\begin{align*}
T^*f(\alpha)=\alpha\circ df_q.
\end{align*}
Therefore
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=\alpha\bigl(df_q(d(f^{-1})_{q'}(d(\tau_{Q'})_\alpha(v)))\bigr).
\end{align*}
Because $f$ is a diffeomorphism, $df_q:T_qQ\to T_{q'}Q'$ and $d(f^{-1})_{q'}:T_{q'}Q'\to T_qQ$ are inverse linear maps. Hence
\begin{align*}
df_q\circ d(f^{-1})_{q'}=\operatorname{id}_{T_{q'}Q'}.
\end{align*}
The expression reduces to
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=\alpha\bigl(d(\tau_{Q'})_\alpha(v)\bigr).
\end{align*}
Finally, this is exactly the defining formula for the tautological one-form $\lambda_{Q'}$ on $T^*Q'$:
\begin{align*}
(\lambda_{Q'})_\alpha(v)=\alpha\bigl(d(\tau_{Q'})_\alpha(v)\bigr).
\end{align*}
Thus
\begin{align*}
\bigl((T^*f)^*\lambda_Q\bigr)_\alpha(v)=(\lambda_{Q'})_\alpha(v).
\end{align*}
[/guided]
[/step]
[step:Conclude equality of one-forms and pass to the canonical symplectic forms]
Since $\alpha\in T^*Q'$ and $v\in T_\alpha(T^*Q')$ were arbitrary, the pointwise equality from the previous step proves
\begin{align*}
(T^*f)^*\lambda_Q=\lambda_{Q'}.
\end{align*}
Using the convention $\omega_Q=-d\lambda_Q$ and $\omega_{Q'}=-d\lambda_{Q'}$, and using the naturality of the exterior derivative under pullback for smooth maps, we compute
\begin{align*}
(T^*f)^*\omega_Q=(T^*f)^*(-d\lambda_Q).
\end{align*}
By linearity of pullback,
\begin{align*}
(T^*f)^*(-d\lambda_Q)=-d\bigl((T^*f)^*\lambda_Q\bigr).
\end{align*}
Substituting the already proved identity for the tautological forms gives
\begin{align*}
-d\bigl((T^*f)^*\lambda_Q\bigr)=-d\lambda_{Q'}.
\end{align*}
Therefore
\begin{align*}
(T^*f)^*\omega_Q=\omega_{Q'}.
\end{align*}
This proves both claimed naturality identities.
[/step]
