Differentiability transfers through a C¹ embedding with injective derivative at an interior point whose image is a neighbourhood

Let $M$, $N$ and $P$ be smooth 3-manifolds with boundary (modelled on the closed half-space), let $i:M\to N$ be a C¹ map that is a topological embedding, and let $x\in M$ be an interior point of $M$ at which the derivative $Di_x$ is injective. Assume that the image $i(M)$ is a neighbourhood of $i(x)$ in $N$. Let $f:N\to P$ be any map. If $f\circ i$ is differentiable at $x$, then

In words: at such a point $i$ is a local C¹ diffeomorphism onto a neighbourhood of $i(x)$, so $f=(f\circ i)\circ i^{-1}$ near $i(x)$. This is a general fact, not stated in the paper; it is the differentiability step behind footnote 2 (the differentiable structure of $W=U\sqcup_\varphi V$ is compatible with those of $U$ and $V$ by restriction), and it is used to transfer differentiability of the time-$t$ maps of the glued field from the pieces to $W$.

Formalization Note "Differentiable at a point" is Mathlib's MDifferentiableAt: continuity at the point and differentiability of the chart representative within the model half-space. The hypothesis that $i(M)$ is a neighbourhood of $i(x)$ is assumed; it also follows from the other hypotheses by the inverse function theorem ($x$ is interior and $Di_x$ is a linear isomorphism), and the embedding hypothesis is then not needed either. No compactness is assumed.