[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*}[/step]

[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: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]