Perspective on the diamond lemma in ring theory As the title indicates, I am seeking some perspective (explained below) on Bergman's diamond lemma (DOI link to Bergman's paper) in ring theory.
I know that it can be used, for instance, to prove the Poincaré-Birkhoff-Witt theorem for universal enveloping algebras.  This is shown in Bergman's original paper.  And then it can be used also for quantized enveloping algebras, quantized function algebras, etc.
I am also aware of this page at Secret Blogging Seminar, which discusses the diamond lemma in the graph-theoretic setting.  It is stated there that this version can be used to prove the Jordan-Hölder theorem on composition series for a finite group (and presumably for modules over a ring, etc).
For this to be a well-formulated question, I need to make clear what I mean by "perspective".  Here is a quote from the introduction to the paper:

The main results in this paper are trivial. But what is trivial when described in
the abstract can be far from clear in the context of a complicated situation where
it is needed.

And then, later, after describing the results, he says:

This fact has been considered obvious and used freely by some ring-theorists
(e.g., [17, Sect. !5l), but others seem unaware of it and write out tortuous
verifications.

So, what I am looking for is examples of situations where the formalism of the diamond lemma really clarified or simplified some algebraic construction, or examples of people writing out "tortuous verifications" when they could have appealed to the diamond lemma instead.
PS  If you've never looked at Bergman's paper before, you should!  It's one of my favorites.  Everything is so clear and well-motivated.  If only I could write like that...
 A: What I believe is really important is that you can use Diamond Lemma to make homological conclusions, and not just prove results on the size of your algebra. For instance, a homogeneous algebra with a quadratic Groebner basis (i.e. with quadratic relations which form a confluent system) is Koszul. Same applies in more tricky case, e.g. operads, where it becomes quite important since verifications become even more torturous (which you might know already from my comment to that SBS entry). 
A: One example of a paper which uses the Diamond Lemma in an algebraic setting is
Michael Hutchings, Integration of singular braid invariants and graph cohomology, 
Transactions of the AMS 350 (1998), 1791-1809. 
See Theorem 4.1  He essentially uses a Diamond Lemma argument, although he never uses the term (not that his argument is any less clear for that).  Further to V. Dotsenko's point, he also essentially proves that the "chord diagram algebra" is Koszul, although he also never uses the word Koszul (probably because he doesn't actually need Koszulness for his purposes).
A: My paper http://arxiv.org/abs/math/0609832 is about some applications of the Diamond Lemma.
A: The thesis  
Moore, E. Graphs of groups: word computations and free crossed
  resolutions. Ph.D. Thesis, University of Wales, Bangor (2001).
considers (following Higgins) a  normal form for  the fundamental groupoid of a graph of groups, and the diamond lemma method is used as a  way of establishing this. Graphs of groupoids are also considered.  The thesis is available as a pdf file here. 
Note that Higgins' method avoids the usual choices of a base point and a tree. 
A: What I totally did not have in mind when writing my first answer to this in 2012 is that the confluence condition of the Diamond Lemma can be interpreted quite nicely in terms of the Maurer-Cartan equation in the resolution of the corresponding monomial algebra, see https://arxiv.org/abs/2010.14792 .
