feat(Order/WellFoundedSet): a set is finite if both a linear order and its opposite order are well founded on it

Mathlib/Order/OrderIsoNat.lean

@@ -10,6 +10,7 @@ public import Mathlib.Logic.Denumerable
 public import Mathlib.Logic.Function.Iterate
 public import Mathlib.Order.Hom.Basic
 public import Mathlib.Data.Set.Subsingleton
+public import Mathlib.Order.InitialSeg
 
 /-!
 # Relation embeddings from the naturals
@@ -76,6 +77,63 @@ theorem not_wellFounded (f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) : ¬Well
   rw [wellFounded_iff_isEmpty, not_isEmpty_iff]
   exact ⟨f⟩
 
+section LinearOrder
+
+variable {α : Type*} {r : α → α → Prop}
+
+theorem infinite_iff_nonempty_relEmbedding_of_isWellOrder [IsWellOrder α r] :
+    Infinite α ↔ Nonempty (((· < ·) : ℕ → ℕ → Prop) ↪r r) := by
+  refine ⟨fun _ ↦ ?_, (·.elim (Infinite.of_injective _ ·.injective))⟩
+  match InitialSeg.total ((· < ·) : ℕ → ℕ → Prop) r with
+  | .inl f => exact ⟨f.toRelEmbedding⟩
+  | .inr g =>
+    match g.principalSumRelIso with
+    | .inr g => exact ⟨g.symm⟩
+    | .inl g =>
+      absurd (‹_› : Infinite α)
+      rw [not_infinite_iff_finite, finite_iff_nonempty_fintype,
+        ← Set.univ_finite_iff_nonempty_fintype]
+      refine Set.Finite.of_finite_image ?_ g.injective.injOn
+      simp [g.range_eq, Set.finite_lt_nat]
+
+theorem finite_iff_empty_relEmbedding_of_isWellOrder [IsWellOrder α r] :
+    Finite α ↔ IsEmpty (((· < ·) : ℕ → ℕ → Prop) ↪r r) := by
+  rw [← not_iff_not, not_finite_iff_infinite, not_isEmpty_iff,
+    infinite_iff_nonempty_relEmbedding_of_isWellOrder (r := r)]
+
+theorem _root_.IsWellOrder.finite_of_isWellOrder_of_isWellOrder_swap
+    [IsWellOrder α r] [IsWellFounded α (Function.swap r)] : Finite α := by
+  rw [finite_iff_empty_relEmbedding_of_isWellOrder (r := r)]
+  have : WellFounded (Function.swap r) := IsWellFounded.wf
+  rw [wellFounded_iff_isEmpty] at this
+  exact Function.isEmpty RelEmbedding.swap
+
+instance (priority := low) _root_.instFiniteOfWellFoundedLTOfWellFoundedGT
+    [LinearOrder α] [WellFoundedLT α] [WellFoundedGT α] : Finite α :=
+  IsWellOrder.finite_of_isWellOrder_of_isWellOrder_swap (r := LT.lt)
+
+theorem infinite_iff_nonempty_relEmbedding_lt_or_nonempty_relEmbedding_gt [IsStrictTotalOrder α r] :
+    Infinite α ↔
+      Nonempty (((· < ·) : ℕ → ℕ → Prop) ↪r r) ∨
+      Nonempty (((· > ·) : ℕ → ℕ → Prop) ↪r r) := by
+  refine ⟨fun inf ↦ ?_, by rintro (h | h) <;> exact h.elim (Infinite.of_injective _ ·.injective)⟩
+  contrapose! inf with h
+  obtain ⟨h_lt, h_gt⟩ := h
+  apply (@Function.isEmpty _ _ · RelEmbedding.swap) at h_lt
+  rw [← wellFounded_iff_isEmpty, ← isWellFounded_iff] at h_gt h_lt
+  have : IsWellOrder α r := ⟨⟩
+  exact IsWellOrder.finite_of_isWellOrder_of_isWellOrder_swap (r := r)
+
+theorem finite_iff_isEmpty_relEmbedding_lt_and_isEmpty_relEmbedding_gt [IsStrictTotalOrder α r] :
+    Finite α ↔
+      IsEmpty (((· < ·) : ℕ → ℕ → Prop) ↪r r) ∧
+      IsEmpty (((· > ·) : ℕ → ℕ → Prop) ↪r r) := by
+  rw [← not_iff_not, Classical.not_and_iff_not_or_not, not_finite_iff_infinite,
+    not_isEmpty_iff, not_isEmpty_iff,
+    infinite_iff_nonempty_relEmbedding_lt_or_nonempty_relEmbedding_gt (r := r)]
+
+end LinearOrder
+
 end RelEmbedding
 
 theorem not_strictAnti_of_wellFoundedLT [Preorder α] [WellFoundedLT α] (f : ℕ → α) :

Mathlib/Order/WellFounded.lean

@@ -82,6 +82,19 @@ instance (r : β → β → Prop) (f : α → β) [IsWellFounded β r] :
     IsWellFounded α (r.onFun f) where
   wf := IsWellFounded.wf.onFun
 
+theorem subtype_iff {p : α → Prop} :
+    WellFounded (α := Subtype p) (Function.onFun r Subtype.val) ↔
+      WellFounded (fun a b ↦ r a b ∧ p a ∧ p b) := by
+  simp_rw [wellFounded_iff_isEmpty_descending_chain, ← not_iff_not (a := IsEmpty _),
+    not_isEmpty_iff, nonempty_subtype]
+  refine ⟨fun ⟨f, ha⟩ ↦ ⟨(f ·), ?_⟩, fun ⟨f, ha⟩ ↦ ⟨(⟨f ·, ?_⟩), ?_⟩⟩ <;> grind
+
+theorem subtype_iff' {p : α → Prop} {r : Subtype p → Subtype p → Prop} :
+    WellFounded r ↔ WellFounded (fun a b ↦ ∃ ha : p a, ∃ hb : p b, r ⟨a, ha⟩ ⟨b, hb⟩) := by
+  simp_rw [wellFounded_iff_isEmpty_descending_chain, ← not_iff_not (a := IsEmpty _),
+    not_isEmpty_iff, nonempty_subtype]
+  refine ⟨fun ⟨f, ha⟩ ↦ ⟨(f ·), ?_⟩, fun ⟨f, ha⟩ ↦ ⟨(⟨f ·, (ha _).snd.fst⟩), ?_⟩⟩ <;> grind
+
 theorem _root_.Function.Injective.isWellOrder (r : β → β → Prop) {f : α → β} (hf : f.Injective)
     [IsWellOrder β r] : IsWellOrder α (r.onFun f) where
   __ := hf.trichotomous_onFun r

Mathlib/Order/WellFoundedSet.lean

@@ -559,6 +559,13 @@ lemma WellFoundedOn.mapsTo {α β : Type*} {r : α → α → Prop} (f : β →
     t.WellFoundedOn (r on f) := by
   exact InvImage.wf (fun x : t ↦ ⟨f x, h x.prop⟩) hw
 
+theorem WellFoundedOn.finite_of_wellFoundedOn_swap {α : Type*} {r : α → α → Prop} {s : Set α}
+    [IsStrictTotalOrder s (Function.onFun r Subtype.val)]
+    (h : WellFoundedOn s r) (h' : WellFoundedOn s (Function.swap r)) :
+    s.Finite := by
+  rw [Set.wellFoundedOn_iff, ← WellFounded.subtype_iff, ← isWellFounded_iff] at h h'
+  exact Set.finite_coe_iff.mp <| @IsWellOrder.finite_of_isWellOrder_of_isWellOrder_swap _ _ ⟨⟩ h'
+
 @[to_dual]
 theorem WellFoundedOn.exists_minimal {α : Type*} [Preorder α] {s : Set α}
     (h : s.WellFoundedOn (· < ·)) (nonempty : s.Nonempty) : ∃ a, Minimal (· ∈ s) a :=