The arbitrary-atlas transported formulation of smooth Poincaré

Let $S^4=\{x\in\mathbb R^5:\|x\|=1\}$, with its subspace topology and standard stereographic smooth structure modeled on $\mathbb R^4$. The proposition $\mathrm{SPC4Pullback}$ states that, for every type $N$ in the base universe equipped with a topology making it compact and Hausdorff, every specified charted-space structure $A$ on $N$ modeled on $\mathbb R^4$ with $C^\infty$-compatible transitions, and every homeomorphism $e:N\to S^4$, there exists a homeomorphism $h:N\to N$ preserving the smooth structure from $A$ on the source to the structure pulled back from $S^4$ along $e$ on the target. The pulled-back atlas consists exactly of $d\circ e$ for sphere atlas charts $d$, with source $e^{-1}(\operatorname{source}(d))$, target $\operatorname{target}(d)$, inverse $e^{-1}\circ d^{-1}$, and preferred chart at $x$ induced by the sphere's preferred chart at $e(x)$. Structure preservation means that for every chart $c$ in $A$ and every sphere atlas chart $d$, the open partial homeomorphism represented by $(d\circ e)\circ h\circ c^{-1}$ belongs to the groupoid of smooth local transformations of $\mathbb R^4$: both it and its inverse are $C^\infty$ on their domains. The choice of $h$ may depend on $e$, and no condition that $h$ be the identity or unique is present. The quantifier over $e$ has no instances if $N$ is empty.