I strongly recommend reading Kenneth Mander's papers in The Philosophy of Mathematical Practice, edited by Paolo Mancosu (you can easily find the volume for download at the usual sites). They are among the best accounts of diagrammatic proofs that I know of (oddly, from a quick glance, I don't see them mentioned in Giaquinto's entry linked in the OP---it's especially odd because Gianquinto also has two contributions to that volume).

Anyway, some of Mander's claims may help to distinguish the algebraic proof of left-cancellation from diagrammatic proofs (incidentally, I found Giaquinto's discussion of the algebraic proof baffling). In particular, he distinguishes exact from co-exact figures of the Euclidean diagrams. Exact features are things like equalities and proportionalities, which "fail immediately upon almost any diagram variation", whereas co-exact features are things like "part-whole relations of regions, segments bounding regions, and lower-dimensional counterparts", that is, properties of the diagram that are "insensitive to the effects of a range of variation in diagram entries". (All quotations from p. 69)

Mander's point is that the diagrams enter in the proof only in order to verify the co-exact features, and never the exact features. I think this is important, because it points to a difference between Euclidean diagrams and the proof of left-cancellation. In the latter case, we are not using any "co-exact" properties of the array of equations to justify the proof, but rather just quantifier rules and substitution, which are logical rules.