A C¹ map with injective derivative at an interior point carries a C¹ local flow to C¹ short-time flow maps of the pushed vector field

Let $M$ and $N$ be smooth 3-manifolds with boundary (modelled on the closed half-space), let $i:M\to N$ be a map of class C¹, and let $X$ and $Z$ be vector fields on $M$ and $N$ with $Di_x(X(x))=Z(i(x))$ for all $x\in M$. Let $x_0$ be an interior point of $M$ at which the derivative $Di_{x_0}$ is injective. An integral curve of a vector field $F$ on a manifold $N$ on a set of times $S\subseteq\mathbb R$ is a curve $\gamma:\mathbb R\to N$ whose derivative within $S$ at every $u\in S$ is $F(\gamma(u))$ (Mathlib's IsMIntegralCurveOn; at the endpoints of an interval the derivative is one-sided). We write $[0,t]$ for the closed interval between $0$ and $t$, in either order (Mathlib's uIcc 0 t). Assume that $X$ has a jointly C¹ local flow at $x_0$: there are $\varepsilon>0$, an open neighbourhood $O$ of $x_0$ and a map $\alpha:M\to\mathbb R\to M$ such that for every $y\in O$ the curve $\alpha(y,\cdot)$ is an integral curve of $X$ on $[-\varepsilon,\varepsilon]$ with $\alpha(y,0)=y$, and $(y,\tau)\mapsto\alpha(y,\tau)$ is of class C¹ on $O\times(-\varepsilon,\varepsilon)$ (the full hypothesis is the conclusion of the companion theorem exists_localFlow_contMDiff_of_isInteriorPoint). A vector field $F$ on a 3-manifold $N$ has local C¹ step maps at a point $p$ if there are $\varepsilon>0$ and an open neighbourhood $O$ of $p$ such that for every $h$ with $|h|\le\varepsilon$ there is a map $f_h:N\to N$ of class C¹ on $O$ with this property: every $y\in O$ is the starting point of an integral curve $\eta$ of $F$ on $[0,h]$ with $\eta(h)=f_h(y)$. Then

In words: by the inverse function theorem, $i$ is a C¹ diffeomorphism from a neighbourhood of $x_0$ onto a neighbourhood of $i(x_0)$ (in particular $i(x_0)$ is an interior point of $N$), and it carries the local flow of $X$ to short-time flow maps of $Z$: $f_h=i\circ\alpha(\cdot,h)\circ i^{-1}$. It is a step of the mission's proof of the C¹ regularity that the proof of Proposition 1.1 (Section 3.1 of arXiv v1, p. 14) takes for granted. There $i$ is one of the two embeddings $i_U$, $i_V$ of a plug gluing and $Z$ is the glued field. The statement covers the points of $W$ that are images of interior points of $U$ or $V$.

Formalization Note The hypothesis on the local flow is the verbatim conclusion of exists_localFlow_contMDiff_of_isInteriorPoint; its clauses on interior points and on uniqueness are part of that conclusion and are not needed for the expected proof. The derivative of $i$ is assumed injective at $x_0$ only; the tangent spaces are 3-dimensional, so it is bijective. $i$ is not assumed to be an embedding. No Hausdorff and no compactness hypothesis is assumed.