First, a preliminary question about Bra-ket notation. On a Hilbert space $H$, the inner product $(\cdot,\cdot):H\times H\to\mathbb C$ gives an identification of a vector ket $\varphi = \vert \varphi\rangle$ with a functional bra $f_\varphi = \langle \varphi\vert$, as $$ (\varphi,\psi) = (\vert\varphi\rangle,\vert\psi\rangle) := f_\varphi(\psi) = \langle \varphi\vert (\vert\psi\rangle)=\langle\varphi\vert\psi\rangle. $$ Here we are not taking the inner product of the ket and the bra, because they lie in different vector spaces (in particular the bra lies in the dual space of $H$). Instead we are defining a bra by $f_\varphi(\psi) = (\varphi,\psi)$ for $\psi\in H$. What exactly is the meaning of $\langle\varphi\vert\psi\rangle$? Just a way of denoting the $(\mathrm{bra},\mathrm{ket})$ pair?
Now let $A$ and $B$ be observables. Suppose there exists a complete set of kets $\{\vert\psi_n\rangle\}$ whose every element is simultaneously an eigenket of $A$ and $B$. Then we says that $A$ and $B$ are compatible. Let $\{a_n\}$ be a sequence of eigenkets of $A$ and $\{b_n\}$ a sequence of eigenkets of $B$. Then we can write $$ AB\vert\psi_n\rangle = Ab_n\vert\psi_n\rangle = a_nb_n\vert\psi_n\rangle = b_na_n\vert\psi_n\rangle = BA\vert\psi_n\rangle. $$ Now, we can expand any arbitrary state ket $\vert\Psi\rangle$ in the complete set $\{\vert\psi_n\rangle\}$ as $$\vert\Psi\rangle = \sum_{n=1}^\infty c_n\vert\psi_n\rangle,$$ where $c_n\in\mathbb C$. So we can see that $$ (AB - BA)\vert\Psi\rangle = \sum_{n=1}^\infty c_n(AB-BA)\vert\psi_n\rangle = 0. $$ This implies that $[A,B]=0$, which means that the operators commute.
My question: what is the meaning of $[A,B]$ in the above line? Is it the commutator of $A$ and $B$? If so, isn't it immediately apparent that $AB-BA=0$ from $AB\vert\psi_n\rangle = BA\vert\psi_n\rangle$? I suppose not, since we went to the effort of showing this implies $AB\vert\Psi\rangle = BA\vert\Psi\rangle$ for an arbitrary $\Psi\in H$. Am I missing anything here?
To answer your questions: