[proofplan]
Choose a smooth bundle atlas for $\pi:E \to N$ and use each local trivialization of $E$ to define an induced local trivialization of the pullback set $f^*E$. The only point requiring verification is compatibility: on overlaps, the transition maps for the pullback bundle are the transition maps of $E$ evaluated at $f(x)$, hence are smooth. These induced charts therefore define a smooth fibre-bundle structure over $M$, make the canonical map $\tilde f$ smooth, and force uniqueness because any structure with the stated property must contain exactly this induced smooth atlas.
[/proofplan]
[step:Construct the induced local product charts on the pullback set]
Regard the pullback set as
\begin{align*}
f^*E:=\{(x,e)\in M\times E: f(x)=\pi(e)\}.
\end{align*}
Let $p:f^*E\to M$ denote the projection $p(x,e)=x$, and let $\tilde f:f^*E\to E$ denote the map $\tilde f(x,e)=e$. Let $\{(V_i,\tau_i)\}_{i \in I}$ be a smooth fibre bundle atlas for $\pi:E \to N$, where each $V_i \subset N$ is open, the family $\{V_i\}_{i \in I}$ covers $N$, and each local trivialization $\tau_i:\pi^{-1}(V_i)\to V_i\times F$ is a diffeomorphism. Let $\operatorname{pr}_{V_i}:V_i\times F\to V_i$ denote the projection onto the first factor. The trivialization satisfies
\begin{align*}
\operatorname{pr}_{V_i} \circ \tau_i = \pi|_{\pi^{-1}(V_i)}.
\end{align*}
For each $i \in I$, define the [open set](/page/Open%20Set) $U_i := f^{-1}(V_i) \subset M$. Since $f$ is continuous, $U_i$ is open, and since the $V_i$ cover $N$, the family $\{U_i\}_{i \in I}$ covers $M$.
Define $\sigma_i:p^{-1}(U_i)\to U_i\times F$ by
\begin{align*}
\sigma_i(x,e)=\left(x,\operatorname{pr}_F(\tau_i(e))\right).
\end{align*}
This map is well-defined: if $(x,e) \in p^{-1}(U_i)$, then $x \in U_i$, so $f(x) \in V_i$; since $(x,e) \in f^*E$, we have $\pi(e)=f(x) \in V_i$, hence $e \in \pi^{-1}(V_i)$ and $\tau_i(e)$ is defined.
Define $\rho_i:U_i\times F\to p^{-1}(U_i)$ by
\begin{align*}
\rho_i(x,a)=\left(x,\tau_i^{-1}(f(x),a)\right).
\end{align*}
Indeed, for $(x,a) \in U_i \times F$, the point $\tau_i^{-1}(f(x),a)$ lies in $\pi^{-1}(V_i)$ and satisfies
\begin{align*}
\pi\left(\tau_i^{-1}(f(x),a)\right)=f(x),
\end{align*}
because $\operatorname{pr}_{V_i}\circ \tau_i=\pi$. Thus $\rho_i(x,a)\in f^*E$ and $p(\rho_i(x,a))=x \in U_i$. Direct substitution gives $\sigma_i\circ \rho_i=\operatorname{id}_{U_i \times F}$ and $\rho_i\circ \sigma_i=\operatorname{id}_{p^{-1}(U_i)}$, so $\sigma_i$ is a bijection.
[guided]
We begin by naming the set and maps being constructed. The pullback set is
\begin{align*}
f^*E:=\{(x,e)\in M\times E: f(x)=\pi(e)\}.
\end{align*}
Its projection to $M$ is the map $p:f^*E\to M$ defined by $p(x,e)=x$, and the canonical map to $E$ is the map $\tilde f:f^*E\to E$ defined by $\tilde f(x,e)=e$. We now take the ordinary bundle charts of $E$ and pull them back along $f$. Let $\tau_i:\pi^{-1}(V_i)\to V_i\times F$ be a local trivialization of $E$. Let $\operatorname{pr}_{V_i}:V_i\times F\to V_i$ denote the projection onto the first factor. The defining condition for a fibre-bundle chart is
\begin{align*}
\operatorname{pr}_{V_i}\circ \tau_i=\pi|_{\pi^{-1}(V_i)}.
\end{align*}
This means that if $\tau_i(e)=(y,a)$, then the base point of $e$ is exactly $y=\pi(e)$.
The pullback bundle should sit over $M$, so the corresponding base open set is
\begin{align*}
U_i:=f^{-1}(V_i).
\end{align*}
This set is open because $f:M\to N$ is continuous. It covers $M$ because the sets $V_i$ cover $N$.
Now define $\sigma_i:p^{-1}(U_i)\to U_i\times F$ by
\begin{align*}
\sigma_i(x,e)=\left(x,\operatorname{pr}_F(\tau_i(e))\right).
\end{align*}
The formula keeps the new base point $x$ and keeps the old fibre coordinate of $e$. The map is well-defined because $(x,e)\in f^*E$ means $f(x)=\pi(e)$. If $x\in U_i$, then $f(x)\in V_i$, hence $\pi(e)\in V_i$, so $e\in \pi^{-1}(V_i)$ and $\tau_i(e)$ is defined.
To see that this is a product chart, we explicitly write its inverse. Define $\rho_i:U_i\times F\to p^{-1}(U_i)$ by
\begin{align*}
\rho_i(x,a)=\left(x,\tau_i^{-1}(f(x),a)\right).
\end{align*}
The point $\tau_i^{-1}(f(x),a)$ lies over $f(x)$ because $\tau_i$ is a bundle trivialization. Therefore
\begin{align*}
\pi\left(\tau_i^{-1}(f(x),a)\right)=f(x),
\end{align*}
so $\left(x,\tau_i^{-1}(f(x),a)\right)$ satisfies the defining equation of $f^*E$. Hence $\rho_i$ maps into $p^{-1}(U_i)$.
Finally, if we start with $(x,a)\in U_i\times F$, then applying $\rho_i$ and then $\sigma_i$ gives back $(x,a)$ because $\tau_i(\tau_i^{-1}(f(x),a))=(f(x),a)$. If we start with $(x,e)\in p^{-1}(U_i)$, then $\tau_i(e)=(f(x),a)$ for $a=\operatorname{pr}_F(\tau_i(e))$, so $\rho_i(\sigma_i(x,e))=(x,e)$. Thus $\sigma_i$ is a bijective local product chart.
[/guided]
[/step]
[step:Verify that the induced product charts have smooth transition maps]
Let $i,j \in I$ and suppose $U_i \cap U_j \neq \varnothing$. Define the overlap set
\begin{align*}
W_{ij}:=V_i \cap V_j \subset N.
\end{align*}
Define $\Theta_{ji}:\tau_i(\pi^{-1}(W_{ij}))\to \tau_j(\pi^{-1}(W_{ij}))$ by
\begin{align*}
\Theta_{ji}(y,a)=\tau_j(\tau_i^{-1}(y,a)).
\end{align*}
Since both $\tau_i$ and $\tau_j$ are smooth bundle charts and preserve base points, there is a smooth map $g_{ji}:W_{ij}\times F\to F$ such that
\begin{align*}
\Theta_{ji}(y,a)=\left(y,g_{ji}(y,a)\right)
\end{align*}
for all $(y,a)\in W_{ij}\times F$.
The pullback transition map is $\sigma_j\circ \sigma_i^{-1}:(U_i\cap U_j)\times F\to (U_i\cap U_j)\times F$. For $(x,a)\in (U_i\cap U_j)\times F$, using $\sigma_i^{-1}(x,a)=\left(x,\tau_i^{-1}(f(x),a)\right)$ gives
\begin{align*}
(\sigma_j\circ \sigma_i^{-1})(x,a)=\left(x,g_{ji}(f(x),a)\right).
\end{align*}
Indeed, this follows by substituting $\sigma_i^{-1}(x,a)=\left(x,\tau_i^{-1}(f(x),a)\right)$ into $\sigma_j$ and then using $\tau_j(\tau_i^{-1}(f(x),a))=(f(x),g_{ji}(f(x),a))$.
The map $(x,a)\mapsto (f(x),a)$ from $(U_i\cap U_j)\times F$ to $W_{ij}\times F$ is smooth because $f$ is smooth, and $g_{ji}$ is smooth by smooth compatibility of the bundle atlas of $E$. Hence $\sigma_j\circ \sigma_i^{-1}$ is smooth. Reversing $i$ and $j$ proves smoothness of the inverse transition map.
[/step]
[step:Define the smooth bundle structure on $f^*E$]
The family
\begin{align*}
\{(p^{-1}(U_i),\sigma_i)\}_{i \in I}
\end{align*}
is an atlas of bijections from subsets of $f^*E$ onto open subsets $U_i\times F$ of $M\times F$, and the preceding step proves that all coordinate changes are smooth. We first verify the topological hypotheses needed for the smooth atlas construction. Equip $f^*E$ with the [subspace topology](/page/Subspace%20Topology) inherited from $M\times E$. Since $M$ and $E$ are Hausdorff and second countable smooth manifolds, the product $M\times E$ is Hausdorff and second countable, and every subspace is Hausdorff and second countable.
For each $i\in I$, the set $p^{-1}(U_i)$ is open in this subspace topology. Indeed,
\begin{align*}
p^{-1}(U_i)=f^*E\cap (U_i\times \pi^{-1}(V_i)).
\end{align*}
The map $\sigma_i:p^{-1}(U_i)\to U_i\times F$ is a homeomorphism for the subspace topology, with inverse $\rho_i(x,a)=\left(x,\tau_i^{-1}(f(x),a)\right)$. To see this, observe that $\sigma_i$ is the restriction to $p^{-1}(U_i)$ of the continuous map $(x,e)\mapsto (x,\operatorname{pr}_F(\tau_i(e)))$, and $\rho_i$ is continuous because it is built from the smooth maps $f$, $\tau_i^{-1}$, and the identity on $U_i$ and $F$. Thus the chart topology agrees locally with the inherited subspace topology.
Therefore the compatible charts satisfy the hypotheses of the smooth atlas construction: the chart domains are open in a Hausdorff, second countable topology, the charts are homeomorphisms onto open subsets of model manifolds, and the transition maps are smooth diffeomorphisms. We equip $f^*E$ with the maximal smooth atlas generated by these compatible product charts; equivalently, this is the unique smooth structure for which every $\sigma_i$ is a diffeomorphism onto $U_i\times F$ and for which the topology is the inherited subspace topology.
With respect to this smooth structure, the projection $p:f^*E\to M$ is the map $p(x,e)=x$. In the chart $\sigma_i$, it is represented by the smooth projection $\operatorname{pr}_{U_i}:U_i\times F\to U_i$, where $\operatorname{pr}_{U_i}(x,a)=x$. Moreover each $\sigma_i$ is a local trivialization of $p$, because
\begin{align*}
\operatorname{pr}_{U_i}\circ \sigma_i=p|_{p^{-1}(U_i)}.
\end{align*}
Thus $p:f^*E\to M$ is a smooth fibre bundle with typical fibre $F$.
[/step]
[step:Verify that every local product chart of $E$ induces a smooth pullback chart]
Let $V\subset N$ be open and let $\tau:\pi^{-1}(V)\to V\times F$ be any smooth local trivialization of $E$. Define $U:=f^{-1}(V)\subset M$ and define $\sigma:p^{-1}(U)\to U\times F$ by
\begin{align*}
\sigma(x,e)=\left(x,\operatorname{pr}_F(\tau(e))\right).
\end{align*}
The same inverse formula as above gives the inverse set map $\rho:U\times F\to p^{-1}(U)$ defined by
\begin{align*}
\rho(x,a)=\left(x,\tau^{-1}(f(x),a)\right),
\end{align*}
so $\sigma$ is a bijective product chart over $U$.
It remains to check that $\sigma$ is smooth for the constructed smooth structure. For each $i\in I$ with $U\cap U_i\neq\varnothing$, define $W_i:=V\cap V_i$. Since $\tau$ and $\tau_i$ are smooth local trivializations of the same smooth bundle $E$, their transition map is smooth. Because both charts preserve base points, there is a smooth map $h_i:W_i\times F\to F$ such that
\begin{align*}
\tau(\tau_i^{-1}(y,a))=\left(y,h_i(y,a)\right)
\end{align*}
for all $(y,a)\in W_i\times F$. On $(U\cap U_i)\times F$, the coordinate representation of $\sigma$ relative to $\sigma_i$ is
\begin{align*}
(\sigma\circ \sigma_i^{-1})(x,a)&=\left(x,h_i(f(x),a)\right).
\end{align*}
This map is smooth because $(x,a)\mapsto (f(x),a)$ is smooth and $h_i$ is smooth. For the reverse coordinate change, define $k_i:W_i\times F\to F$ by the smooth bundle transition formula
\begin{align*}
\tau_i(\tau^{-1}(y,a))=\left(y,k_i(y,a)\right)
\end{align*}
for all $(y,a)\in W_i\times F$. Then on $(U\cap U_i)\times F$,
\begin{align*}
(\sigma_i\circ\sigma^{-1})(x,a)=\left(x,k_i(f(x),a)\right).
\end{align*}
This map is smooth because $(x,a)\mapsto(f(x),a)$ is smooth and $k_i$ is smooth. Hence $\sigma$ is compatible with the constructed maximal atlas and is therefore a smooth local trivialization of $f^*E$ over $U$.
[guided]
The subtle point is that a product chart induced from an arbitrary trivialization $\tau$ of $E$ must be compatible with the atlas already used to build the smooth structure on $f^*E$. Fix $i\in I$ with $U\cap U_i\neq\varnothing$, and set $W_i:=V\cap V_i$. Since $\tau$ and $\tau_i$ are smooth local trivializations of the same smooth fibre bundle over $W_i$, their transition map preserves the base coordinate and has the form
\begin{align*}
\tau(\tau_i^{-1}(y,a))=\left(y,h_i(y,a)\right),
\end{align*}
where $h_i:W_i\times F\to F$ is smooth.
Now compute the coordinate representation of the induced pullback chart $\sigma$ in the already constructed chart $\sigma_i$. For $(x,a)\in (U\cap U_i)\times F$, we have
\begin{align*}
\sigma_i^{-1}(x,a)=\left(x,\tau_i^{-1}(f(x),a)\right),
\end{align*}
and therefore
\begin{align*}
(\sigma\circ \sigma_i^{-1})(x,a)=\left(x,h_i(f(x),a)\right).
\end{align*}
This is smooth because the map $(x,a)\mapsto(f(x),a)$ from $(U\cap U_i)\times F$ to $W_i\times F$ is smooth and $h_i$ is smooth.
Compatibility also requires the reverse transition. Since $\tau_i\circ\tau^{-1}$ is a smooth transition map preserving base points, there is a smooth map $k_i:W_i\times F\to F$ such that
\begin{align*}
\tau_i(\tau^{-1}(y,a))=\left(y,k_i(y,a)\right)
\end{align*}
for all $(y,a)\in W_i\times F$. Thus
\begin{align*}
(\sigma_i\circ\sigma^{-1})(x,a)=\left(x,k_i(f(x),a)\right),
\end{align*}
which is smooth for the same reason. Hence $\sigma$ is compatible with every chart $\sigma_i$ on overlaps, so it belongs to the constructed maximal atlas and is a smooth local trivialization of $f^*E$ over $U$.
[/guided]
[/step]
[step:Check that the canonical map to $E$ is smooth]
We prove smoothness of the map $\tilde f:f^*E\to E$ defined by $\tilde f(x,e)=e$ in local coordinates. On $p^{-1}(U_i)$, use the pullback chart $\sigma_i:p^{-1}(U_i)\to U_i\times F$ on the domain and the bundle chart $\tau_i:\pi^{-1}(V_i)\to V_i\times F$ on the target. The coordinate representation $\tau_i\circ \tilde f\circ \sigma_i^{-1}:U_i\times F\to V_i\times F$ is
\begin{align*}
(\tau_i\circ \tilde f\circ \sigma_i^{-1})(x,a)=(f(x),a).
\end{align*}
This map is smooth because $f:U_i\to V_i$ is smooth and the fibre coordinate $a\in F$ is unchanged. Since smoothness is local on the source and target, $\tilde f$ is smooth.
[/step]
[step:Prove uniqueness from the required induced trivializations]
Let $\mathcal{S}$ be any smooth fibre bundle structure on the same set $f^*E$ over $M$ satisfying the stated property: for every local trivialization $\tau:\pi^{-1}(V)\to V\times F$ of $E$, the induced map $\sigma:p^{-1}(f^{-1}(V))\to f^{-1}(V)\times F$ defined by
\begin{align*}
\sigma(x,e)=\left(x,\operatorname{pr}_F(\tau(e))\right)
\end{align*}
is a smooth local trivialization. In particular, all charts $\sigma_i$ constructed above are smooth charts for $\mathcal{S}$.
The smooth structure constructed above is the maximal smooth atlas generated by the induced charts $\{\sigma_i\}_{i\in I}$. Since $\mathcal{S}$ contains these same induced charts and is a smooth atlas compatible with them, every chart of $\mathcal{S}$ is compatible with the maximal atlas generated by the $\sigma_i$. Conversely, every chart in the maximal atlas generated by the $\sigma_i$ is compatible with the smooth atlas of $\mathcal{S}$. Therefore the two maximal smooth atlases coincide.
Hence the smooth fibre-bundle structure on $f^*E$ satisfying the stated induced-chart condition is unique. This completes the construction of the pullback bundle and the proof of the theorem.
[/step]