[proofplan]
The proof is the fibre-product universal property specialized to principal bundles. We define the candidate map by pairing the base point of $q \in Q$ with its image in $P$, namely $\widetilde H(q) = (\rho(q), H(q))$. The compatibility equation $\pi \circ H = f \circ \rho$ proves that this pair lies in $f^*P$, the smooth fibre-product structure gives smoothness, and $G$-equivariance follows directly from the equivariance of $H$. Finally, the two projection identities force this formula, so uniqueness is immediate.
[/proofplan]
[step:Define the map into the fibre product]
Define a map
\begin{align*}
\widetilde H: Q \to f^*P, \quad q \mapsto (\rho(q), H(q)).
\end{align*}
This is well-defined because, for every $q \in Q$,
\begin{align*}
f(\rho(q)) = (\pi \circ H)(q) = \pi(H(q)).
\end{align*}
Thus $(\rho(q),H(q)) \in f^*P$ by the defining equation of the pullback bundle.
[guided]
We need a map into $f^*P$, whose points are pairs $(x,p) \in N \times P$ satisfying the compatibility condition $f(x)=\pi(p)$. Since $q \in Q$ already determines a point $\rho(q) \in N$ and the given map $H:Q \to P$ determines a point $H(q) \in P$, the only possible candidate is
\begin{align*}
\widetilde H: Q \to f^*P, \quad q \mapsto (\rho(q), H(q)).
\end{align*}
The only point that requires verification is that this pair actually belongs to $f^*P$. The hypothesis $\pi \circ H = f \circ \rho$ says precisely that, for each $q \in Q$,
\begin{align*}
\pi(H(q)) = f(\rho(q)).
\end{align*}
This is exactly the fibre-product condition. Hence $(\rho(q),H(q)) \in f^*P$ for every $q \in Q$, so $\widetilde H$ is a well-defined map from $Q$ to the pullback bundle.
[/guided]
[/step]
[step:Verify smoothness using the fibre-product smooth structure]
Let
\begin{align*}
K: Q \to N \times P, \quad q \mapsto (\rho(q), H(q))
\end{align*}
be the product map. Since $\rho:Q \to N$ and $H:Q \to P$ are smooth, the map $K$ is smooth. Its image lies in the embedded submanifold $f^*P \subset N \times P$ by the previous step. By the defining smooth structure on the fibre product, the induced map $\widetilde H:Q \to f^*P$ is smooth.
[/step]
[step:Check the two projection identities]
For every $q \in Q$, the projection to $N$ gives
\begin{align*}
(\operatorname{pr}_N \circ \widetilde H)(q) = \operatorname{pr}_N(\rho(q),H(q)) = \rho(q).
\end{align*}
Therefore $\operatorname{pr}_N \circ \widetilde H = \rho$. Similarly, the projection to $P$ gives
\begin{align*}
(\operatorname{pr}_P \circ \widetilde H)(q) = \operatorname{pr}_P(\rho(q),H(q)) = H(q).
\end{align*}
Thus $\operatorname{pr}_P \circ \widetilde H = H$.
[/step]
[step:Prove equivariance with respect to the right $G$-actions]
Let $g \in G$ and $q \in Q$. Since $\rho:Q \to N$ is the bundle projection of a principal $G$-bundle, $\rho(q\cdot g)=\rho(q)$. Since $H:Q \to P$ is $G$-equivariant, $H(q\cdot g)=H(q)\cdot g$. Hence
\begin{align*}
\widetilde H(q\cdot g) = (\rho(q\cdot g),H(q\cdot g)) = (\rho(q),H(q)\cdot g).
\end{align*}
By the definition of the right action on $f^*P$,
\begin{align*}
(\rho(q),H(q)\cdot g) = (\rho(q),H(q))\cdot g = \widetilde H(q)\cdot g.
\end{align*}
Therefore $\widetilde H$ is $G$-equivariant.
[/step]
[step:Show uniqueness from the two coordinate projections]
Let $L:Q \to f^*P$ be a smooth $G$-equivariant map satisfying $\operatorname{pr}_N \circ L = \rho$ and $\operatorname{pr}_P \circ L = H$. For each $q \in Q$, the point $L(q) \in f^*P \subset N \times P$ is determined by its two coordinates. Therefore
\begin{align*}
L(q) = ((\operatorname{pr}_N \circ L)(q),(\operatorname{pr}_P \circ L)(q)) = (\rho(q),H(q)) = \widetilde H(q).
\end{align*}
Thus $L=\widetilde H$. The constructed map is therefore the unique principal bundle morphism over $\operatorname{id}_N$ whose composition with $\operatorname{pr}_P$ is $H$.
[/step]
