[proofplan]
We prove both directions directly from bases. If the dimensions are equal, choose bases of $V$ and $W$ with the same finite number of elements and define a linear map by sending the basis vectors of $V$ to the corresponding basis vectors of $W$. This map has an explicitly constructed inverse, hence is a $k$-linear isomorphism. Conversely, a $k$-linear isomorphism sends a basis of $V$ to a basis of $W$, so the two bases have the same cardinality and therefore the same dimension.
[/proofplan]
[step:Construct an isomorphism from bases with equal cardinality]
Assume
\begin{align*}
\dim_k V = \dim_k W.
\end{align*}
Let $n$ be the nonnegative integer equal to this common dimension.
Let $0_V \in V$ and $0_W \in W$ denote the zero vectors of $V$ and $W$, respectively.
If $n = 0$, then $V = \{0_V\}$ and $W = \{0_W\}$. Define
\begin{align*}
T: V &\to W
\end{align*}
to be the unique map satisfying $T(0_V) = 0_W$. This map is $k$-linear, injective, and surjective, so it is a $k$-vector space isomorphism.
Now assume $n \ge 1$. Choose a basis $(v_1,\dots,v_n)$ of $V$ over $k$ and a basis $(w_1,\dots,w_n)$ of $W$ over $k$. Define
\begin{align*}
T: V &\to W
\end{align*}
by declaring that, for the unique coordinate expression
\begin{align*}
v = \sum_{i=1}^n a_i v_i
\end{align*}
with $a_1,\dots,a_n \in k$,
\begin{align*}
T(v) = \sum_{i=1}^n a_i w_i.
\end{align*}
The uniqueness of coordinates in the basis $(v_1,\dots,v_n)$ makes $T$ well-defined.
To prove linearity, let $v,u \in V$ and let $\lambda \in k$. Write
\begin{align*}
v = \sum_{i=1}^n a_i v_i
\end{align*}
and
\begin{align*}
u = \sum_{i=1}^n b_i v_i
\end{align*}
with $a_i,b_i \in k$. Then
\begin{align*}
v+\lambda u = \sum_{i=1}^n (a_i+\lambda b_i)v_i.
\end{align*}
Therefore
\begin{align*}
T(v+\lambda u) = \sum_{i=1}^n (a_i+\lambda b_i)w_i.
\end{align*}
By distributivity in the vector space $W$,
\begin{align*}
T(v+\lambda u) = \sum_{i=1}^n a_i w_i + \lambda \sum_{i=1}^n b_i w_i.
\end{align*}
Thus
\begin{align*}
T(v+\lambda u) = T(v)+\lambda T(u),
\end{align*}
so $T$ is $k$-linear.
Define also
\begin{align*}
S: W &\to V
\end{align*}
by the rule that, for the unique expression
\begin{align*}
w = \sum_{i=1}^n c_i w_i
\end{align*}
with $c_1,\dots,c_n \in k$,
\begin{align*}
S(w) = \sum_{i=1}^n c_i v_i.
\end{align*}
To verify linearity of $S$, let $w,z \in W$ and $\mu \in k$. Write
\begin{align*}
w = \sum_{i=1}^n c_i w_i
\end{align*}
and
\begin{align*}
z = \sum_{i=1}^n d_i w_i
\end{align*}
with $c_i,d_i \in k$. Then
\begin{align*}
w + \mu z = \sum_{i=1}^n (c_i + \mu d_i) w_i.
\end{align*}
Hence
\begin{align*}
S(w + \mu z) = \sum_{i=1}^n (c_i + \mu d_i) v_i = \sum_{i=1}^n c_i v_i + \mu \sum_{i=1}^n d_i v_i = S(w) + \mu S(z).
\end{align*}
Therefore $S$ is $k$-linear. Let $\operatorname{id}_V: V \to V$ and $\operatorname{id}_W: W \to W$ denote the identity maps on $V$ and $W$, respectively. For each $v = \sum_{i=1}^n a_i v_i \in V$,
\begin{align*}
S(T(v)) = S\left(\sum_{i=1}^n a_i w_i\right) = \sum_{i=1}^n a_i v_i = v.
\end{align*}
For each $w = \sum_{i=1}^n c_i w_i \in W$,
\begin{align*}
T(S(w)) = T\left(\sum_{i=1}^n c_i v_i\right) = \sum_{i=1}^n c_i w_i = w.
\end{align*}
Hence $S \circ T = \operatorname{id}_V$ and $T \circ S = \operatorname{id}_W$. Therefore $T$ is a $k$-linear isomorphism from $V$ to $W$.
[guided]
Assume
\begin{align*}
\dim_k V = \dim_k W.
\end{align*}
Let $n$ be the nonnegative integer equal to the common value of these two dimensions. Let $0_V \in V$ and $0_W \in W$ denote the zero vectors of $V$ and $W$, respectively. The argument is to choose one basis in each space and match the basis vectors one by one. The only edge case is $n = 0$, where there are no basis vectors to list.
If $n = 0$, the zero-dimensionality means that the empty set is a basis of each space. Therefore every vector in $V$ is the zero vector $0_V$, and every vector in $W$ is the zero vector $0_W$. Thus $V = \{0_V\}$ and $W = \{0_W\}$. Define
\begin{align*}
T: V &\to W
\end{align*}
by $T(0_V)=0_W$. This is the only possible function from $V$ to $W$. It is $k$-linear because it sends the zero vector to the zero vector and there are no other vectors to check. It is injective because its domain has one element, and it is surjective because its image contains the only element of $W$. Hence $T$ is a $k$-vector space isomorphism.
Now suppose $n \ge 1$. Choose a basis $(v_1,\dots,v_n)$ of $V$ over $k$ and a basis $(w_1,\dots,w_n)$ of $W$ over $k$. We define a map by sending each $v_i$ to the corresponding $w_i$ and extending linearly. More explicitly, every $v \in V$ has a unique coordinate expression
\begin{align*}
v = \sum_{i=1}^n a_i v_i
\end{align*}
with $a_1,\dots,a_n \in k$. Define
\begin{align*}
T: V &\to W
\end{align*}
by
\begin{align*}
T(v) = \sum_{i=1}^n a_i w_i.
\end{align*}
Why is this well-defined? The coefficients $a_1,\dots,a_n$ are unique because $(v_1,\dots,v_n)$ is a basis. Thus the formula assigns exactly one vector of $W$ to each vector of $V$.
We verify that $T$ is $k$-linear. Let $v,u \in V$ and let $\lambda \in k$. Write
\begin{align*}
v = \sum_{i=1}^n a_i v_i
\end{align*}
and
\begin{align*}
u = \sum_{i=1}^n b_i v_i
\end{align*}
with $a_i,b_i \in k$. Since addition and scalar multiplication are computed coordinatewise in a basis,
\begin{align*}
v+\lambda u = \sum_{i=1}^n (a_i+\lambda b_i)v_i.
\end{align*}
Applying the definition of $T$ gives
\begin{align*}
T(v+\lambda u) = \sum_{i=1}^n (a_i+\lambda b_i)w_i.
\end{align*}
Using distributivity in $W$, this becomes
\begin{align*}
T(v+\lambda u) = \sum_{i=1}^n a_i w_i + \lambda \sum_{i=1}^n b_i w_i.
\end{align*}
By the definitions of $T(v)$ and $T(u)$, we conclude
\begin{align*}
T(v+\lambda u) = T(v)+\lambda T(u).
\end{align*}
So $T$ is $k$-linear.
To prove that $T$ is an isomorphism, we construct its inverse explicitly. Every $w \in W$ has a unique expression
\begin{align*}
w = \sum_{i=1}^n c_i w_i
\end{align*}
with $c_1,\dots,c_n \in k$. Define
\begin{align*}
S: W &\to V
\end{align*}
by
\begin{align*}
S(w) = \sum_{i=1}^n c_i v_i.
\end{align*}
This map reverses the correspondence between the two bases. We verify that $S$ is $k$-linear. Let $w,z \in W$ and let $\mu \in k$. Write
\begin{align*}
w = \sum_{i=1}^n c_i w_i
\end{align*}
and
\begin{align*}
z = \sum_{i=1}^n d_i w_i
\end{align*}
with $c_i,d_i \in k$. Since addition and scalar multiplication are computed coordinatewise in the basis $(w_1,\dots,w_n)$,
\begin{align*}
w + \mu z = \sum_{i=1}^n (c_i + \mu d_i) w_i.
\end{align*}
Applying the definition of $S$ gives
\begin{align*}
S(w + \mu z) = \sum_{i=1}^n (c_i + \mu d_i) v_i.
\end{align*}
Using distributivity in $V$,
\begin{align*}
S(w + \mu z) = \sum_{i=1}^n c_i v_i + \mu \sum_{i=1}^n d_i v_i.
\end{align*}
By the definitions of $S(w)$ and $S(z)$,
\begin{align*}
S(w + \mu z) = S(w) + \mu S(z).
\end{align*}
Therefore $S$ is $k$-linear.
Let $\operatorname{id}_V: V \to V$ and $\operatorname{id}_W: W \to W$ denote the identity maps on $V$ and $W$, respectively. Now check the compositions. If $v = \sum_{i=1}^n a_i v_i$, then
\begin{align*}
S(T(v)) = S\left(\sum_{i=1}^n a_i w_i\right) = \sum_{i=1}^n a_i v_i = v.
\end{align*}
Thus $S \circ T = \operatorname{id}_V$. Similarly, if $w = \sum_{i=1}^n c_i w_i$, then
\begin{align*}
T(S(w)) = T\left(\sum_{i=1}^n c_i v_i\right) = \sum_{i=1}^n c_i w_i = w.
\end{align*}
Thus $T \circ S = \operatorname{id}_W$. Since $T$ has a two-sided inverse $S$, the map $T$ is bijective. Since $T$ is also $k$-linear, it is a $k$-vector space isomorphism from $V$ to $W$.
[/guided]
[/step]
[step:Show that an isomorphism sends a basis to a basis]
Conversely, assume that there exists a $k$-vector space isomorphism
\begin{align*}
\Phi: V &\to W.
\end{align*}
Since $V$ is finite-dimensional, choose a basis $(v_1,\dots,v_m)$ of $V$ over $k$, where $m$ is a nonnegative integer. If $m = 0$, then $V=\{0_V\}$. Because $\Phi$ is bijective, $W=\{0_W\}$, so $\dim_k W=0=\dim_k V$.
Assume now that $m \ge 1$. Define the ordered list
\begin{align*}
(\Phi(v_1),\dots,\Phi(v_m))
\end{align*}
of vectors in $W$. We show that it is a basis of $W$.
First, it spans $W$. Let $w \in W$. Since $\Phi$ is surjective, there exists $v \in V$ such that $\Phi(v)=w$. Since $(v_1,\dots,v_m)$ spans $V$, there exist $a_1,\dots,a_m \in k$ such that
\begin{align*}
v = \sum_{i=1}^m a_i v_i.
\end{align*}
Using linearity of $\Phi$,
\begin{align*}
w = \Phi(v) = \Phi\left(\sum_{i=1}^m a_i v_i\right) = \sum_{i=1}^m a_i \Phi(v_i).
\end{align*}
Thus $(\Phi(v_1),\dots,\Phi(v_m))$ spans $W$.
Second, it is linearly independent. Suppose $a_1,\dots,a_m \in k$ satisfy
\begin{align*}
\sum_{i=1}^m a_i \Phi(v_i) = 0_W.
\end{align*}
By linearity of $\Phi$,
\begin{align*}
\Phi\left(\sum_{i=1}^m a_i v_i\right) = 0_W.
\end{align*}
Since $\Phi$ is injective and $\Phi(0_V)=0_W$, it follows that
\begin{align*}
\sum_{i=1}^m a_i v_i = 0_V.
\end{align*}
Because $(v_1,\dots,v_m)$ is linearly independent, $a_i=0$ for every $i \in \{1,\dots,m\}$. Therefore $(\Phi(v_1),\dots,\Phi(v_m))$ is linearly independent.
Hence $(\Phi(v_1),\dots,\Phi(v_m))$ is a basis of $W$ with $m$ elements. Therefore
\begin{align*}
\dim_k W = m = \dim_k V.
\end{align*}
This proves the converse implication.
[/step]
[step:Conclude the equivalence]
The first step proves that equality of dimensions implies the existence of a $k$-vector space isomorphism $V \to W$. The second step proves that the existence of a $k$-vector space isomorphism $V \to W$ implies equality of dimensions. Therefore $V$ and $W$ are isomorphic as vector spaces over $k$ if and only if
\begin{align*}
\dim_k V = \dim_k W.
\end{align*}
[/step]
