Smoothness of the parameter derivative of a family of holomorphic maps

Let $S=H^{-1}(1)\subset\mathbb R^{2n+2}$ be strictly star-shaped, $J$ a compatible complex structure on $\xi$, and $\tilde J$ the induced almost complex structure on $\mathbb R^{2n+2}\setminus\{0\}$. Let $l\ge 2$, $r\in\mathbb R$, and let $g:\mathbb C\times\mathbb R\to\mathbb R^{2n+2}$ be of class $C^l$ on $\mathbb C\times(-r,r)$, such that for every $t\in(-r,r)$ the map $g(\cdot,t)$ is smooth, avoids $0$ and is $\tilde J$-holomorphic on $\mathbb C$. Then for every $t\in(-r,r)$ the map $z\mapsto\partial_t g(z,t)$ is smooth.

The statement upgrades the regularity of the parameter derivative of a family of holomorphic maps, so that infinitesimal deformations of a holomorphic plane can be treated as smooth sections.

Formalization Note: $\partial_t g(z,t)$ is fderiv ℝ g (z, t) (0, 1); JHolomorphic.IsJHolomorphicOn (Jtilde H J) Set.univ f means $f$ is differentiable and $\partial_s f+\tilde J(f)\,\partial_t f=0$ on $\mathbb C$.