[proofplan] First we strengthen the differential of $f$ along $H_0$ to a vector-bundle isomorphism extending $df$ and preserving the ambient symplectic forms. The only nontrivial point is the hypersurface linear algebra: the restricted two-form has a one-dimensional characteristic kernel, and the missing transverse derivative can be chosen so that all transverse pairings match. A tubular-neighbourhood extension then realizes this prescribed first-order data by a local diffeomorphism. Pulling back $\omega_1$ gives a symplectic form agreeing with $\omega_0$ along $H_0$, and the [relative Moser lemma](/theorems/10051) corrects the preliminary extension to an exact local symplectomorphism. [/proofplan]

[step:Identify the characteristic line bundles preserved by $df$] For $i\in\{0,1\}$, define the restricted two-form \begin{align*} \beta_i:=j_i^*\omega_i\in \Omega^2(H_i). \end{align*} Since $H_i$ is a hypersurface in a symplectic manifold, each fiber \begin{align*} K_{i,x}:=\ker((\beta_i)_x)\subset T_xH_i \end{align*} is one-dimensional. Indeed, $T_xH_i$ has codimension one in the symplectic [vector space](/page/Vector%20Space) $(T_xM_i,(\omega_i)_x)$, so its symplectic orthogonal has dimension one and is contained in $T_xH_i$. Define the characteristic line bundle $K_i\subset TH_i$ by $(K_i)_x:=K_{i,x}$ for $x\in H_i$. The hypothesis says \begin{align*} f^*\beta_1=\beta_0. \end{align*} Thus, for $x\in H_0$, $v\in T_xH_0$, and $k\in K_{0,x}$, \begin{align*} (\beta_1)_{f(x)}(df_x(k),df_x(v))=(\beta_0)_x(k,v)=0. \end{align*} Because $df_x:T_xH_0\to T_{f(x)}H_1$ is an isomorphism, this implies \begin{align*} df_x(K_{0,x})=K_{1,f(x)}. \end{align*} Therefore $df$ identifies the characteristic line bundle $K_0:=\ker\beta_0$ with $f^*K_1$. [/step]

[step:Choose the transverse derivative so the ambient forms agree along $H_0$]We construct a smooth vector-bundle isomorphism \begin{align*} A:TM_0|_{H_0}\to f^*TM_1|_{H_1} \end{align*} covering $f$, satisfying $A|_{TH_0}=df$ and \begin{align*} (\omega_1)_{f(x)}(A_xu,A_xv)=(\omega_0)_x(u,v) \end{align*} for every $x\in H_0$ and every $u,v\in T_xM_0$. Choose smooth line subbundles $N_i\subset TM_i|_{H_i}$ such that \begin{align*} TM_i|_{H_i}=TH_i\oplus N_i. \end{align*} Such complements exist because $H_i$ is embedded and the relevant vector bundles are smooth over a paracompact manifold. Let \begin{align*} q_i:TM_i|_{H_i}\to TM_i|_{H_i}/TH_i \end{align*} denote the quotient maps. For each $i$, the map \begin{align*} TM_i|_{H_i}/TH_i \to K_i^*, \qquad [v] \mapsto \bigl(k\mapsto \omega_i(k,v)\bigr) \end{align*} is a smooth line-bundle isomorphism. It is well-defined because every $k\in K_i$ annihilates $TH_i$ under $\omega_i$. It is injective because if $\omega_i(k,v)=0$ for every $k\in K_i$, then $v$ lies in the symplectic orthogonal of $K_i$, which equals $TH_i$ for a hypersurface, so $[v]=0$. Using this isomorphism and the already established identification $df:K_0\to f^*K_1$, define the normal quotient map \begin{align*} \overline A:TM_0|_{H_0}/TH_0\to f^*(TM_1|_{H_1}/TH_1) \end{align*} as the unique line-bundle isomorphism satisfying \begin{align*} (\omega_1)_{f(x)}(df_x(k),\overline A_x([v]))=(\omega_0)_x(k,v) \end{align*} for every $x\in H_0$, $k\in K_{0,x}$, and $v\in T_xM_0$. Now let $n\in N_{0,x}$. Choose the representative of $\overline A([n])$ in the fixed line $N_{1,f(x)}$ and call it $n_1^0$. Define a linear functional \begin{align*} \ell_{x,n}:T_xH_0\to \mathbb R \end{align*} by \begin{align*} \ell_{x,n}(w):=(\omega_0)_x(w,n)-(\omega_1)_{f(x)}(df_x(w),n_1^0). \end{align*} By the defining property of $\overline A$, this functional vanishes on $K_{0,x}$. Hence it descends to a functional on $T_xH_0/K_{0,x}$. The two-form $\beta_0$ induces a nondegenerate skew form on $T_xH_0/K_{0,x}$, and $df_x$ identifies this quotient with $T_{f(x)}H_1/K_{1,f(x)}$. Therefore there is a unique class $[u_1]\in T_{f(x)}H_1/K_{1,f(x)}$ such that \begin{align*} (\beta_1)_{f(x)}(df_x(w),u_1)=\ell_{x,n}(w) \end{align*} for every $w\in T_xH_0$. Choosing a smooth complement to $K_1$ in $TH_1$ gives a smooth representative $u_1$ of this class. Define \begin{align*} A_x(w+n):=df_x(w)+n_1^0+u_1 \end{align*} for $w\in T_xH_0$ and $n\in N_{0,x}$. This definition is linear in $w+n$ and smooth in $x$. It extends $df$ on $TH_0$, has normal quotient $\overline A$, and is therefore a vector-bundle isomorphism. For two tangent vectors in $T_xH_0$, preservation of the form is exactly $f^*\beta_1=\beta_0$. For one tangent vector and one normal vector, the definition of $u_1$ gives the desired equality. Finally, the pairing of the normal vector with itself is zero for both skew-symmetric forms. Thus $A_x^*(\omega_1)_{f(x)}=(\omega_0)_x$ for every $x\in H_0$.[/step]

[guided]The issue is that $df$ only acts on $TH_0$, while we need a derivative on all of $TM_0|_{H_0}$. Since $H_0$ is a hypersurface, the missing direction is one-dimensional. However, the restricted form $\beta_0=j_0^*\omega_0$ is degenerate, so we must first understand exactly which direction it loses. For $i\in\{0,1\}$, define \begin{align*} \beta_i:=j_i^*\omega_i\in \Omega^2(H_i). \end{align*} At each point $x\in H_i$, the kernel \begin{align*} K_{i,x}:=\ker((\beta_i)_x)\subset T_xH_i \end{align*} is a line. The reason is linear algebra in a symplectic vector space: $T_xH_i$ has codimension one in $T_xM_i$, so its symplectic orthogonal has dimension one, and for a hypersurface this orthogonal line lies inside $T_xH_i$. The hypothesis \begin{align*} f^*\beta_1=\beta_0 \end{align*} implies that $df$ carries this kernel line to the corresponding kernel line. Indeed, if $k\in K_{0,x}$ and $v\in T_xH_0$, then \begin{align*} (\beta_1)_{f(x)}(df_x(k),df_x(v))=(\beta_0)_x(k,v)=0. \end{align*} Since $df_x:T_xH_0\to T_{f(x)}H_1$ is surjective, $df_x(k)$ annihilates all of $T_{f(x)}H_1$ under $\beta_1$, so $df_x(k)\in K_{1,f(x)}$. Now choose smooth complements \begin{align*} TM_i|_{H_i}=TH_i\oplus N_i. \end{align*} The normal quotient $TM_i|_{H_i}/TH_i$ is a line bundle. It is paired nondegenerately with the characteristic line $K_i$ by the ambient symplectic form: \begin{align*} [v]\mapsto \bigl(k\mapsto \omega_i(k,v)\bigr). \end{align*} This is well-defined because $k\in K_i$ pairs to zero with all tangent vectors in $TH_i$. It is an isomorphism because if the normal class $[v]$ pairs to zero with $K_i$, then $v$ lies in the symplectic orthogonal of $K_i$, which is $TH_i$, so $[v]=0$. This pairing tells us how to choose the normal quotient of the desired derivative. We define \begin{align*} \overline A:TM_0|_{H_0}/TH_0\to f^*(TM_1|_{H_1}/TH_1) \end{align*} to be the unique line-bundle map satisfying \begin{align*} (\omega_1)_{f(x)}(df_x(k),\overline A_x([v]))=(\omega_0)_x(k,v) \end{align*} for all $k\in K_{0,x}$ and $v\in T_xM_0$. This fixes the transverse scaling. There is still a second correction to make. Fix $x\in H_0$ and $n\in N_{0,x}$. A representative $n_1^0$ of the normal class $\overline A_x([n])$ may not pair correctly with every tangent vector $df_x(w)$, only with the characteristic direction. Define the error functional \begin{align*} \ell_{x,n}:T_xH_0\to \mathbb R \end{align*} by \begin{align*} \ell_{x,n}(w):=(\omega_0)_x(w,n)-(\omega_1)_{f(x)}(df_x(w),n_1^0). \end{align*} The construction of $\overline A$ makes $\ell_{x,n}$ vanish on $K_{0,x}$, so it descends to $T_xH_0/K_{0,x}$. On this quotient, $\beta_0$ is nondegenerate, and $df_x$ identifies it with the quotient $T_{f(x)}H_1/K_{1,f(x)}$. Hence there is a unique class $[u_1]\in T_{f(x)}H_1/K_{1,f(x)}$ satisfying \begin{align*} (\beta_1)_{f(x)}(df_x(w),u_1)=\ell_{x,n}(w) \end{align*} for all $w\in T_xH_0$. Choosing a smooth complement of $K_1$ in $TH_1$ gives a smooth representative $u_1$. Finally set \begin{align*} A_x(w+n):=df_x(w)+n_1^0+u_1. \end{align*} This map extends $df$ on $TH_0$. Its induced map on the normal quotient is the line-bundle isomorphism $\overline A_x$, while its restriction to $T_xH_0$ is the vector-space isomorphism $df_x$; hence $A_x:T_xM_0\to T_{f(x)}M_1$ is an isomorphism for every $x\in H_0$, and these isomorphisms vary smoothly with $x$. It preserves $\omega$ on pairs of tangent vectors by the hypothesis $f^*\beta_1=\beta_0$. It preserves the pairing between tangent and normal vectors by the defining equation for $u_1$. It preserves normal-normal pairings because both sides are zero by skew-symmetry. Therefore \begin{align*} A_x^*(\omega_1)_{f(x)}=(\omega_0)_x \end{align*} for every $x\in H_0$.[/guided]

[step:Realize the prescribed derivative by a diffeomorphism of neighbourhoods] By the [tubular neighbourhood theorem](/theorems/2276) with prescribed first jet along an embedded submanifold, applied to the embedded hypersurfaces $H_i\subset M_i$, the diffeomorphism $f:H_0\to H_1$, and the smooth vector-bundle isomorphism \begin{align*} A:TM_0|_{H_0}\to f^*TM_1|_{H_1} \end{align*} extending $df$ and fiberwise invertible over $f$, the prescribed first-order data are realized by a diffeomorphism \begin{align*} G:V_0\to V_1 \end{align*} between open neighbourhoods $V_i\subset M_i$ of $H_i$, with $G|_{H_0}=f$ and \begin{align*} dG_x=A_x \end{align*} for every $x\in H_0$. Define \begin{align*} \widetilde\omega_1:=G^*\omega_1\in\Omega^2(V_0). \end{align*} Since $\omega_1$ is closed and nondegenerate and $G$ is a diffeomorphism, $\widetilde\omega_1$ is a symplectic form on $V_0$. For every $x\in H_0$ and every $u,v\in T_xM_0$, \begin{align*} (\widetilde\omega_1)_x(u,v)=(\omega_1)_{f(x)}(dG_xu,dG_xv)=(\omega_1)_{f(x)}(A_xu,A_xv)=(\omega_0)_x(u,v). \end{align*} Thus $\widetilde\omega_1$ and $\omega_0$ agree along $H_0$ as ambient two-forms on $TM_0|_{H_0}$. [/step]

[step:Apply the relative Moser lemma to correct the preliminary extension] The two forms $\omega_0|_{V_0}$ and $\widetilde\omega_1$ are symplectic forms on the common neighbourhood $V_0$ of $H_0$, and they agree along $H_0$ as ambient two-forms. Since both forms are closed on $V_0$, the straight-line family \begin{align*} \omega_t:=(1-t)\omega_0+t\widetilde\omega_1 \end{align*} consists of closed two-forms. Since $\omega_t$ equals $\omega_0$ at every point of $H_0$ and nondegeneracy is an open condition on alternating forms, after shrinking $V_0$ to a smaller open neighbourhood of $H_0$, each $\omega_t$ is symplectic for every $t\in[0,1]$. The hypotheses of the [citetheorem:10051] are satisfied on the common neighbourhood $V_0$: the forms $\omega_0|_{V_0}$ and $\widetilde\omega_1$ are closed symplectic forms, they agree along $H_0$ as ambient two-forms, and after the preceding shrinking the straight-line forms $\omega_t$ are symplectic for every $t\in[0,1]$. Equivalently, the closed difference $\widetilde\omega_1-\omega_0$ vanishes along $H_0$ and therefore has the relative primitive required in the Moser argument after shrinking. Applying the lemma with $N=H_0$, $\omega_0$, and $\widetilde\omega_1$, there exist an open neighbourhood $U_0\subset V_0$ of $H_0$, an open neighbourhood $W_0\subset V_0$ of $H_0$, and a diffeomorphism \begin{align*} \psi:U_0\to W_0 \end{align*} such that $\psi|_{H_0}=\operatorname{id}_{H_0}$ and \begin{align*} \psi^*\widetilde\omega_1=\omega_0 \end{align*} on $U_0$. [/step]

[step:Compose the Moser correction with the preliminary extension] Define the map \begin{align*} F:U_0 \to M_1, \qquad x \mapsto G(\psi(x)) \end{align*} Let \begin{align*} U_1:=F(U_0)\subset M_1. \end{align*} Since $G$ and $\psi$ are diffeomorphisms onto their images, $F:U_0\to U_1$ is a diffeomorphism. For $x\in H_0$, \begin{align*} F(x)=G(\psi(x))=G(x)=f(x), \end{align*} so $F|_{H_0}=f$. Finally, \begin{align*} F^*\omega_1=\psi^*(G^*\omega_1)=\psi^*\widetilde\omega_1=\omega_0. \end{align*} This proves the required local symplectic extension of $f$. [/step]