Let $P$ be a $\mathsf{Set}$-valued presheaf and let $f^\ast:\mathsf{PSh}(Y)\rightarrow \mathsf{PSh}(X)$ be the (topological) inverse image sheaf functor, defined on objects as the filtered colimit $$(f^\ast P)(U)=\varinjlim_{V\supset f(U)}PV,\;\;\;V\text{ open}$$ I'm trying to prove $(f^\ast P)_x=P_{f(x)}$ by abstract nonsense. So just writing definitions down ($U$ is open): $$(f^\ast P)_x= \varinjlim_{U\ni x}f^\ast P(U)=\varinjlim_{U\ni x} \varinjlim_{V\supset f(U)}PV$$ I think I should say something along the lines of "since colimits commute with colimits, the RHS is equal to $\varinjlim_{V\supset f(U):U\ni x}PV$, which is itself equal to $\varinjlim_{V\ni f(X)}PV$."
Unfortunately, I'm not sure how to formalize the use of the "colimits commute with colimits theorem", nor how to make the leap from $V\supset f(U):U\ni x$ to $V\ni f(x)$.
How do I proceed?
Here is an abstract nonsense proof for sheaves.
Given a continuous map $f : X \to Y$, we get a functor $f_* : \mathbf{Sh} (X) \to \mathbf{Sh} (Y)$, defined on objects by $f_* A (V) = A (f^{-1} V)$. The assignment $f \mapsto f_*$ is clearly functorial. But a point $x$ in $X$ is given by a continuous map $x : 1 \to X$, so $f_* x_* = f (x)_*$; hence $x^* f^* \cong f (x)^*$, because the left adjoint of the composite is the composite of the left adjoints. But $x^*$ (resp. $f (x)^*$) is precisely the functor taking a sheaf on $X$ (resp. $Y$) to the stalk at $x$ (resp. $f (x)$).