Gluing plugs (from the proof of Béguin–Bonatti–Yu, Prop. 1.1): near the maximal invariant sets the glued flow is the flow of the pieces

Let $(U,X)$ and $(V,Y)$ be plugs: $X$, $Y$ are nonsingular C¹ vector fields on the compact Hausdorff 3-manifolds with boundary $U$, $V$, transverse to the boundary. Let $T^{out}$ be a union of connected components of $\partial^{out}U$, let $T^{in}$ be a union of connected components of $\partial^{in}V$, and let $\varphi:U\to V$ be any map (no continuity is assumed, and $\varphi$ is not assumed to map $T^{out}$ into $T^{in}$; $T^{in}$ occurs in no other hypothesis). Let $(W,Z)$ be a gluing of $(U,X)$ and $(V,Y)$ along $\varphi$: C¹ embeddings $i_U:U\to W$ and $i_V:V\to W$ with injective derivatives cover the compact Hausdorff 3-manifold $W$, identify exactly the points $x\in T^{out}$ with $\varphi(x)$, and satisfy $Di_U(X)=Z\circ i_U$, $Di_V(Y)=Z\circ i_V$. Write $\Lambda_X$, $\Lambda_Y$ for the maximal invariant sets (points whose orbit is defined for all times) and $X^t$, $Y^t$, $Z^t$ for the time-$t$ maps of the flows. Then:

1. for every $x\in\Lambda_X$, the image $i_U(U)$ is a neighbourhood of $i_U(x)$ in $W$, and for every real $t$ there is a neighbourhood $O$ of $x$ in $U$ with

2. for every $y\in\Lambda_Y$, the image $i_V(V)$ is a neighbourhood of $i_V(y)$ in $W$, and for every real $t$ there is a neighbourhood $O$ of $y$ in $V$ with

In words: near each point of $\Lambda_X$ (resp. $\Lambda_Y$) the time-$t$ map of $Z$ is the time-$t$ map of $X$ (resp. $Y$) read through the embedding, and the image of the piece is a neighbourhood of the image of that point. This is what the proof of Proposition 1.1 takes for granted when, in its fourth and fifth sentences, it treats $\Lambda_X$ and $\Lambda_Y$ as hyperbolic sets of $Z$ (footnote 2: the differentiable structure of $W$ is compatible with those of $U$ and $V$ by restriction).

Formalization Note The time-$t$ map $X^t$ is the mission's flowMap: when some integral curve of $X$ through $x$ is defined on the closed time interval between $0$ and $t$, $X^t(x)$ is the value at time $t$ of a chosen such curve; otherwise $X^t(x)=x$. Nothing in the definition asserts that this choice is unique. The derivative $D(X^t)_x$ is Mathlib's mfderiv, which is $0$ where $X^t$ is not differentiable. The identity cannot hold on all of $U$: a point whose $X$-orbit leaves $U$ before time $t$ has $X^t(y)=y$ by convention, while its $Z$-orbit can continue in $W$. So the conjugacy is stated on a neighbourhood of each $x\in\Lambda_X$ (Mathlib's ∀ᶠ y in 𝓝 x), which is also what the comparison of derivatives needs; its proof needs continuous dependence of the orbits of the C¹ field $X$ on initial conditions (so that orbits of points near $x\in\Lambda_X$ stay in $U$ up to time $t$) together with uniqueness of integral curves of $Z$ inside $i_U(\operatorname{int}U)$ (the lifting lemma integralCurve_lift_of_embedding and the uniqueness theorem for C¹ fields at interior points). The neighbourhood statements follow from $\Lambda_X\cap\partial U=\emptyset$, $\Lambda_Y\cap\partial V=\emptyset$ (transversality, normalCoord_nonneg_of_hasMFDerivWithinAt) and the inverse function theorem: at an interior point $y$ the derivative $D(i_V)_y$ is a linear isomorphism, so $i_V$ maps a neighbourhood of $y$ onto an open subset of $W$ (and likewise for $i_U$ at points of $\Lambda_X$). The statement carries no hypothesis on $\varphi$ (none is in the parent statement). $Z$ is not assumed to be C¹; it is controlled only through the embeddings.