mathlib
8b14d48f - feat(logic/relation): Transitive closure of well-founded relation is well-founded (#13698)
