Pushforward definition question. Using notations from wikipedia. If $\phi: M \to N$ is a smooth map with derivative map $d\phi_x: T_xM \to T_{\phi(x)}N.$
The pushforward of $X$ by $\phi$ is $$d\phi_x(X)f := X(f\circ \phi).  \tag{1}$$
where $f \in C^\infty(N).$
Now I know $X \in T_pM$ as a tangent vector is a derivation acting on functions in $C^\infty(M).$ So as wikipedia says, $d\phi_x(X)$ is a tangent vector in $T_{\phi(x)}N$ derivation acting on functions in $C^\infty(N)$. Then isn't $X$ still acting on functions on $M$ in this definition in equation (1) ? All this defintion did was pullback $f$, but $X$ is still a tangent vector on $T_xM$ not $T_{\phi(x)}N.$
Also on page 53 of John Lee's Intro to Smooth manifold book, where he denotes $\nu = X$ here in wiki notation. He notes $\nu \in T_pM$ but calls it a derivation at $F(p)$ ($F$ is our $\phi$ here).
 A: In your equation $(1)$, $f$ is not a function on $M$ but a function on $N$. So the vector $Y = d\phi_x(X)$, which we want to be an element of $T_{\phi(x)} N$, acts on functions on $N$.
Now, how you define the action of the vector $Y$ is a completely different business. Yes, you use the action of $X$ on functions on $M$ to define the action of $Y$: you take the function $f: N \rightarrow \mathbb R$ and transport it to a function $f \circ \phi: M \rightarrow \mathbb R$, then apply $X$ to this (new) function. But the fact remains that in this way, your $Y$ takes functions on $N$ and returns numbers, and it does so as a derivation.
To be more specific, $Y = d\phi_x(X)$ is a derivation at $\phi(x)$. What this means is that it takes equivalence classes of functions from an open neighborhood of $\phi(x)$ to $\mathbb R$, where two functions are equivalent iff they are equal on an open neighborhood of $\phi(x)$, and returns a real number for each such equivalence class, and it does this respecting the Leibniz rule.
Let $[f]$ be such an equivalence class, with a representative $f: U \rightarrow \mathbb R$, where $\phi(x) \in U$ and $U \subset N$ is open.
To specify the vector $Y \in T_{\phi(x)} N$, it's enough to specify its values on every such class $[f]$, and then to check that the specification you give satisfies the Leibniz rule - this is just because that is what a vector at $\phi(x)$ is, it is precisely such a specification of some values for each class $[f]$.
So we specify the values as such: we put by definition $Y([f]):= X([g])$, where $g$ is the function $g: \phi^{-1}(U) \rightarrow \mathbb R$, $g := f \circ \phi\vert_{\phi^{-1}(U)}$ where since $\phi(x) \in U$ and $\phi$ is continuous, $\phi^{-1}(U)$ is an open neighborhood of $x$, so $g$ does indeed define a class like the ones $X$ takes as argument.
Now it's immediate to check that since $X([g])$ doesn't depend on the representative we choose for the class $[g]$, neither does $Y$ depend on the representative $f$. Indeed, suppose $f:U \rightarrow \mathbb R$, $f_1: V \rightarrow \mathbb R$ are two functions such that $\phi(x) \in W \subset U \cap V$ where $W$ is an open set with $f|_W = f_1|_W$. Then $f_1 \circ \phi|_{\phi^{-1}(V)}$ coincides with $f \circ \phi|_{\phi^{-1}(U)}$ on $\phi^{-1}(W)$, so, since $X$ is a vector, $X([f_1 \circ \phi|_{\phi^{-1}(V)}]) = X( [f \circ \phi|_{\phi^{-1}(U)}] )$.
One can also easily see that $Y$ satisfies the Leibniz rule, using that $X$ satisfies it: for two classes of functions $[f], [g]$ at $\phi(x)$ we have that
\begin{align*}
Y([f]\cdot[g]) &\stackrel{\textrm{ def $[f]\cdot[g]$}}{=} Y([fg]) 
\stackrel{\textrm{ def $Y$}}{=} X ([(fg)\circ\phi)]) \\
&=X([ (f \circ \phi) \cdot (g \circ \phi) ]) \\
&=(f \circ \phi)(x) X([g\circ \phi]) + (g \circ \phi)(x) X([f\circ \phi])
\textrm{ (bcs. $X$ satisfies Leibniz) } \\
&=f(\phi(x)) Y([g]) + g(\phi(x)) Y([f])
\end{align*}
But the condition
$$
Y([f]\cdot[g]) = f(\phi(x)) Y([g]) + g(\phi(x)) Y([f])
$$
is precisely what it means for $Y$ to satisfy the Leibniz rule at $\phi(x)$.
So $Y$ is a vector at $\phi(x)$ by definition: it maps equivalence classes of local functions at $\phi(x)$ on $N$ to numbers satisfying the Leibniz rule, and this is by definition what a vector does.
