Following this thread, I'm trying to prove in detail the chain rule to unveil the subtle machinery. Could you have a check on my proof?
Let $X \subseteq \mathbb R^M$, $Y \subseteq \mathbb R^N$, and $Z \subseteq \mathbb R^P$ be $m$-, $n$-, and $p$-dimensional smooth manifolds respectively. Let $f:X \to Y$ and $g:Y \to Z$ be smooth. Fix $x \in X$. Let $\varphi:U \to V$, $\psi:A \to B$, and $\eta:E \to F$ be local parameterizations around $x$, $f(x)$, and $g \circ f(x)$ respectively.
There exists $A'$ open in $A$ such that $\psi^{-1} \circ f (x) \in A'$ and $t := \eta^{-1} \circ g \circ \psi_{\restriction A'}$ is well-defined, i.e., the domains and images of functions in the composition are compatible.
Similarly, there exists $U'$ open in $U$ such that $\varphi^{-1} (x) \in U'$ and $h := \psi^{-1} \circ f \circ \varphi_{\restriction U'}$ is well-defined.
Also, there exists $U''$ open in $U$ such that $\varphi^{-1} (x) \in U''$ and $k := \eta^{-1} \circ (g \circ f) \circ \varphi_{\restriction U''}$ is well-defined.
Composition of smooth maps is smooth, so $t,h,k$ are smooth. Wlog, we assume $U' =U''$ such that $\operatorname{im} h \subseteq A'$.
The derivative of $f$ at $x$ is $$\mathrm d f_x := \mathrm d \psi_{\psi^{-1} \circ f (x)} \circ \mathrm d h_{\varphi^{-1} (x)} \circ (\mathrm d \varphi_{\varphi^{-1} (x)})^{-1}.$$
The derivative of $g$ at $f(x)$ is $$\mathrm d g_{f (x)} := \mathrm d \eta_{\eta^{-1} \circ g \circ f (x)} \circ \mathrm d t_{\psi^{-1} \circ f (x)} \circ (\mathrm d \psi_{\psi^{-1} \circ f (x)})^{-1}.$$
The derivative of $g \circ f$ at $x$ is $$\mathrm d (g \circ f)_{x} := \mathrm d \eta_{\eta^{-1} \circ g \circ f (x)} \circ \mathrm d k_{\varphi^{-1} (x)} \circ (\mathrm d \varphi_{\varphi^{-1} (x)})^{-1}.$$
It follows that \begin{align} & \mathrm d g_{f (x)} \circ \mathrm d f_x \\ ={} & \left ( \mathrm d \eta_{\eta^{-1} \circ g \circ f (x)} \circ \mathrm d t_{\psi^{-1} \circ f (x)} \circ (\mathrm d \psi_{\psi^{-1} \circ f (x)})^{-1} \right ) \circ \left ( \mathrm d \psi_{\psi^{-1} \circ f (x)} \circ \mathrm d h_{\varphi^{-1} (x)} \circ (\mathrm d \varphi_{\varphi^{-1} (x)})^{-1} \right ) \\ ={} & \mathrm d \eta_{\eta^{-1} \circ g \circ f (x)} \circ \mathrm d t_{\psi^{-1} \circ f (x)} \circ \mathrm d h_{\varphi^{-1} (x)} \circ (\mathrm d \varphi_{\varphi^{-1} (x)})^{-1}. \end{align}
Notice that $t$ and $h$ are smooth functions whose domain is open in a Euclidean space, so we can apply the chain rule. We have \begin{align} & \mathrm d k_{\varphi^{-1} (x)} \\ ={} & \mathrm d \big (\eta^{-1} \circ (g \circ f) \circ \varphi_{\restriction U'} \big)_{\varphi^{-1} (x)} \\ ={} & \mathrm d \big (\eta^{-1} \circ g \circ \psi_{\restriction A'} \circ \psi^{-1} \circ f \circ \varphi_{\restriction U'} \big)_{\varphi^{-1} (x)} \quad \text{because} \quad \operatorname{im} h \subseteq A'\\ ={} & \mathrm d (t \circ h)_{\varphi^{-1} (x)} \\ ={} & \mathrm d t_{h \circ \varphi^{-1} (x)} \circ \mathrm d h_{\varphi^{-1} (x)} \quad \text{by chain rule} \\ ={} & \mathrm d t_{\psi^{-1} \circ f (x)} \circ \mathrm d h_{\varphi^{-1} (x)}. \end{align}
Hence $$\mathrm d g_{f (x)} \circ \mathrm d f_x = \mathrm d \eta_{\eta^{-1} \circ g \circ f (x)} \circ \mathrm d k_{\varphi^{-1} (x)} \circ (\mathrm d \varphi_{\varphi^{-1} (x)})^{-1} = \mathrm d (g \circ f)_{x}.$$
This completes the proof.