WellFounded.exists_well_order_ge

theorem WellFounded.exists_well_order_ge : ∀ {α : Type u} {r : α → α → Prop}, WellFounded r → ∃ s, r ≤ s ∧ IsWellOrder α s

This theorem states that for any well-founded relation `r` on a type `α`, there exists a well-ordering `s` on that same type `α` such that `r` is a subset of `s`. A well-founded relation is one where there are no infinite descending chains, and a well-ordering is a total order with the property that every non-empty subset has a least element. So in essence, this theorem says that any well-founded relation can be extended to a well-ordering on the same type.

More concisely: Given a well-founded relation on a type, there exists a well-ordering that is an extension of the relation.