Why are monoidal categories interesting?
And the tensor product (addition in this case) has some special properties –
so saying that this picture proves that actually means that you can read a proof off the diagram in a straightforward way:
So all the things that “look like they would work” according to the picture actually do work in practice because our tensor product thing is associative and because addition works nicely with the relationship. But in a follow up blog post, they talk about something more outrageous: you can (using vector space duality) take the lines in one of these diagrams and move them backwards and make loops. Some of the diagrams in this post are sort of why I got interested in that area in the first place – I thought it was really cool that you could formally define / prove things with pictures.
Source: jvns.ca