I'm practicing my diagram chasing and reasoning skills, and, as an exercise, I'm trying to prove that if a category has products and also has a terminal object $\mathbf 1$, then for any $a$ an object of the category, $a \times \mathbf 1 \cong a$ (that's also exercise III.8.4 in Goldblatt's "Topoi"). I'm also trying to do that rigorously without leaving any "obvious" steps out.
So consider this diagram:
Here, $f_1$ and $f_2$ are some morphisms we don't have any prior information about, they'll be determined later.
First consider the right half (starting with $a$). $<1_a, \mathbf 1_a>$ exists and makes the right half commute by definition of the product. In particular, $1_a = \pi_a \circ <1_a, \mathbf 1_a>$.
Now we need to show that $1_{a \times \mathbf 1} = <1_a, \mathbf 1_a> \circ \pi_a$, and this is more interesting. Let's draw $a \times \mathbf 1$ to the left of $a$ along with the morphisms as on the diagram.
The upper left triangle we've just formed commutes because $\pi_a = 1_a \circ \pi_a$ by definition of $1_a$. This also implies that the whole upper straight triangle commutes (*).
Let's take $f_1$ to be something that makes the lower left triangle commute: $\mathbf 1_a \circ \pi_a$ will do. This also implies that the whole bottom straight triangle commutes (**).
Next, since $\mathbf 1$ is terminal, $f_1$ is actually forced to be $\pi_{\mathbf 1}$, and this means that taking $f_2 = 1_{a \times \mathbf 1}$ makes the diagram commute. On the other hand, $<1_a, \mathbf 1_a> \circ \pi_a$ also makes the diagram commute, which follows from (*) and (**). But this means precisely that $1_{a \times \mathbf 1} = <1_a, \mathbf 1_a> \circ \pi_a$, as needed.
Does it seem reasonable? Can I do better?
This is a small nitpick, but since there's a unique choice of $f_1$, $f_2$ which makes the diagram commute, I don't think it's wise to say "$f_1$ and $f_2$ are some morphisms we don't have any prior information about, they'll be determined later." Better to just tell the reader $f_1 = \mathbf{1}_a \circ \pi_a$ and $f_2 = \langle{1_a, \mathbf{1}_a}\rangle \circ \pi_a$, since we do have enough prior information to conclude this if we want the diagram to commute! That's just my opinion on proof style, though, and you should feel free to ignore it.
This leads into a discussion of the only small error in your proof. You say "taking $f_2 = 1_{a \times \mathbf{1}}$ makes the diagram commute" but you can only conclude this if you already know that $1_{a \times \mathbf{1}} = \langle 1_a, \mathbf{1}_a \rangle \circ \pi_a$! The reason for this is that of course $1_{a \times \mathbf{1}} = \langle 1_a, \mathbf{1}_a \rangle \circ \pi_a$ must hold if the diagram does commute, and the composition $\langle 1_a, \mathbf{1}_a \rangle \circ \pi_a$ cannot be written as a different composition of maps in the diagram (in particular, $\pi_a$ is the unique incoming arrow to $a$ and $\langle{1_a, \mathbf{1}_a}\rangle$ is the unique incoming arrow to $a \times \mathbf{1}$).
You're on the right track here, though. You should make explicit the proof that $1_{a \times \mathbf{1}} = \langle 1_a, \mathbf{1}_a \rangle \circ \pi_a$ by using the fact that $1_{a \times \mathbf{1}} = \langle{\pi_a, \pi_{\mathbf{1}}}\rangle = \langle{\pi_a, f_1}\rangle$. Hope this helps!