I will give a gentle introduction to the Diamond Lemma. This is a useful technique to prove that certain “PBW-type” bases exist of algebras given by generators and relations. In particular, we will see the PBW theorem for usual Lie algebras.