[Merged by Bors] - feat: port #18527

Mathlib/Order/InitialSeg.lean

@@ -4,7 +4,7 @@
 Authors: Mario Carneiro, Floris van Doorn
 
 ! This file was ported from Lean 3 source module order.initial_seg
-! leanprover-community/mathlib commit 8da9e30545433fdd8fe55a0d3da208e5d9263f03
+! leanprover-community/mathlib commit 1a313d8bba1bad05faba71a4a4e9742ab5bd9efd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -215,6 +215,13 @@
   rfl
 #align initial_seg.le_add_apply InitialSeg.leAdd_apply
 
+protected theorem acc (f : r ≼i s) (a : α) : Acc r a ↔ Acc s (f a) :=
+  ⟨by
+    refine' fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => _
+    obtain ⟨a', rfl⟩ := f.init hb
+    exact ha _ (f.map_rel_iff.mp hb), f.toRelEmbedding.acc a⟩
+#align initial_seg.acc InitialSeg.acc
+
 end InitialSeg
 
 /-!
@@ -424,8 +431,34 @@
   (@ofIsEmpty _ _ EmptyRelation _ _ PUnit.unit) fun _ => not_false
 #align principal_seg.pempty_to_punit PrincipalSeg.pemptyToPunit
 
+protected theorem acc [IsTrans β s] (f : r ≺i s) (a : α) : Acc r a ↔ Acc s (f a) :=
+  (f : r ≼i s).acc a
+#align principal_seg.acc PrincipalSeg.acc
+
 end PrincipalSeg
 
+/-- A relation is well-founded iff every principal segment of it is well-founded.
+
+In this lemma we use `subrel` to indicate its principal segments because it's usually more
+convenient to use.
+-/
+theorem wellFounded_iff_wellFounded_subrel {β : Type _} {s : β → β → Prop} [IsTrans β s] :
+    WellFounded s ↔ ∀ b, WellFounded (Subrel s { b' | s b' b }) :=
+  by
+  refine'
+    ⟨fun wf b => ⟨fun b' => ((PrincipalSeg.ofElement _ b).acc b').mpr (wf.apply b')⟩, fun wf =>
+      ⟨fun b => Acc.intro _ fun b' hb' => _⟩⟩
+  let f := PrincipalSeg.ofElement s b
+  obtain ⟨b', rfl⟩ := f.down.mp ((PrincipalSeg.ofElement_top s b).symm ▸ hb' : s b' f.top)
+  exact (f.acc b').mp ((wf b).apply b')
+#align well_founded_iff_well_founded_subrel wellFounded_iff_wellFounded_subrel
+
+theorem wellFounded_iff_principalSeg.{u} {β : Type u} {s : β → β → Prop} [IsTrans β s] :
+    WellFounded s ↔ ∀ (α : Type u) (r : α → α → Prop) (_ : r ≺i s), WellFounded r :=
+  ⟨fun wf _ _ f => RelHomClass.wellFounded f.toRelEmbedding wf, fun h =>
+    wellFounded_iff_wellFounded_subrel.mpr fun b => h _ _ (PrincipalSeg.ofElement s b)⟩
+#align well_founded_iff_principal_seg wellFounded_iff_principalSeg
+
 /-! ### Properties of initial and principal segments -/