The diamond lemma, a.k.a. Newman's lemma, which says that a terminating system is globally confluent if and only if it is locally confluent has a very simple proof based on Noetherian induction. This proof was first published by Gérard Huet in 1980; see the Wikipedia article.

But this lemma has many nontrivial applications and, somewhat like the example of linearity of expectation mentioned elsewhere, it can often seem amazing that the possibly very complicated ways in which paths can diverge is irrelevant as long as local steps can be corrected.

The diamond lemma, a.k.a. Newman's lemma, which says that a terminating system is globally confluent if and only if it is locally confluent, has a very simple proof based on Noetherian induction. This proof was first published by Gérard Huet in 1980; see the Wikipedia article.

But this lemma has many nontrivial applications and, somewhat like the example of linearity of expectation mentioned elsewhere, it can often seem amazing that the possibly very complicated ways in which paths can diverge is irrelevant as long as local steps can be corrected.