I'm just exploring other proofs now
$$\begin{array}{rcccl} \mathcal M_n(k[A][t]) & \overset {f^\ast} \longrightarrow & \mathcal M_n(\mathcal M_n(k[t])) \\ \downarrow {\small \det} & & \downarrow {\small \det} \\ k[A][t] & \overset f \longrightarrow & \mathcal M_n(k[t]) & \overset {g^*} \longrightarrow & \mathcal M_n(k[A]) \\ & & \downarrow {\small \det} & & \downarrow {\small \det} \\ & & k[t] & \overset g \longrightarrow & k[A] \end{array}$$
$g$ sends $t$ to $A$ as usual
we have $tI-A \in k[A][t]$
CH says $g(\det(f(tI-A))) = O$
note that $k[A]$ is a commutative ring
we have a monic division algorithm for polynomials over commutative rings
$\det(tI-A) I_n \in \mathcal M_n(k[t])$
$\det(tI-A)I_n \in k[A][t]$ as well, but this needs more justification
let's just suppose $\det(tI-A) = \sum c_i t^i$
$\det(tI-A)I_n = (\sum c_i t^i) I_n = \sum c_i (I_n t^i) \in k[A][t]$. This is the justification
Now by monic division algorithm, $\sum c_i (I_n t^i) = (I_nt - A)B + C$ where $C \in k[A]$.
now $k[A][t]$ is a polynomial ring over a commutative ring, and comes with an evaluation homomorphism $\phi_A : k[A][t] \to k[A]$ sending $I_n t$ to $A$
$\phi_A(\sum c_i (I_n t^i)) = \phi_A((I_nt - A)B + C) = (\phi_A(I_nt) - \phi_A(A)) \phi_A(B) + \phi_A(C) = (A - A) \phi_A(B) + C = C$
$\sum c_i (I_n t^i) \in k[A][t]$
$f(\sum c_i (I_n t^i)) = \det(tI-A) \in k[t]$
$f(\sum c_i (I_n t^i)) I_n \in \mathcal M_n(k[t])$
$f(\sum c_i (I_n t^i)) I_n = \det(tI-A) I_n = (tI-A) \operatorname{adj}(tI-A) \in \mathcal M_n(k[t])$ (sorry, there's no escape from using adjugate)
$f(\sum c_i (I_n t^i)) I_n = f((I_n t - A) B + C) I_n = (tI - A) B + C$
[inconsistent notation: $I$ vs $I_n$: they mean exactly the same here]
so $(tI-A)B + C = (tI-A) \operatorname{adj}(tI-A)$
by counting degrees, $B=\operatorname{adj}(tI-A)$ and $C=O$, qed
so the diagram above is really the wrong diagram
btw $f$ is given through $f(\sum_i (\sum_j c_{ij} A^j) t^i) = \sum_i \sum_j c_{ij} t^i A^j$
