From 1c56a8de7cbb31a04ff0a52fd5339541d565a9bc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Mon, 17 Jan 2022 10:14:49 +0000
Subject: [PATCH] feat(order/well_founded_set): Antichains in a partial well
 order are finite (#11286)

and when the relation is reflexive and symmetric, it's actually an equivalent condition.
---
 src/data/set/finite.lean        |  9 ++++
 src/order/well_founded_set.lean | 76 ++++++++++++++++++++++++---------
 2 files changed, 66 insertions(+), 19 deletions(-)

diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index 78be07136c41f..078a24e054ae5 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -420,6 +420,15 @@ theorem infinite.exists_lt_map_eq_of_maps_to [linear_order α] {s : set α} {t :
 let ⟨x, hx, y, hy, hxy, hf⟩ := hs.exists_ne_map_eq_of_maps_to hf ht
 in hxy.lt_or_lt.elim (λ hxy, ⟨x, hx, y, hy, hxy, hf⟩) (λ hyx, ⟨y, hy, x, hx, hyx, hf.symm⟩)
 
+lemma finite.exists_lt_map_eq_of_range_subset [linear_order α] [_root_.infinite α] {t : set β}
+  {f : α → β} (hf : range f ⊆ t) (ht : finite t) :
+  ∃ a b, a < b ∧ f a = f b :=
+begin
+  rw [range_subset_iff, ←maps_univ_to] at hf,
+  obtain ⟨a, -, b, -, h⟩ := (@infinite_univ α _).exists_lt_map_eq_of_maps_to hf ht,
+  exact ⟨a, b, h⟩,
+end
+
 theorem infinite_range_of_injective [_root_.infinite α] {f : α → β} (hi : injective f) :
   infinite (range f) :=
 by { rw [←image_univ, infinite_image_iff (inj_on_of_injective hi _)], exact infinite_univ }
diff --git a/src/order/well_founded_set.lean b/src/order/well_founded_set.lean
index 5c735e0e3ee78..e74fbe18c3ac9 100644
--- a/src/order/well_founded_set.lean
+++ b/src/order/well_founded_set.lean
@@ -3,10 +3,10 @@ Copyright (c) 2021 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import data.set.finite
-import order.well_founded
-import order.order_iso_nat
 import algebra.pointwise
+import order.antichain
+import order.order_iso_nat
+import order.well_founded
 
 /-!
 # Well-founded sets
@@ -39,6 +39,10 @@ A well-founded subset of an ordered type is one on which the relation `<` is wel
  * `set.is_wf.union` shows that the union of two well-founded subsets is well-founded.
  * `finset.is_wf` shows that all `finset`s are well-founded.
 
+## TODO
+
+Prove that `s` is partial well ordered iff it has no infinite descending chain or antichain.
+
 ## References
  * [Higman, *Ordering by Divisibility in Abstract Algebras*][Higman52]
  * [Nash-Williams, *On Well-Quasi-Ordering Finite Trees*][Nash-Williams63]
@@ -202,6 +206,53 @@ theorem partially_well_ordered_on.image_of_monotone_on {s : set α}
     exact (classical.some_spec (h n)).1 }
 end
 
+lemma _root_.is_antichain.finite_of_partially_well_ordered_on {s : set α} {r : α → α → Prop}
+  (ha : is_antichain r s) (hp : s.partially_well_ordered_on r) :
+  s.finite :=
+begin
+  refine finite_or_infinite.resolve_right (λ hi, _),
+  obtain ⟨m, n, hmn, h⟩ := hp (λ n, hi.nat_embedding _ n) (range_subset_iff.2 $
+    λ n, (hi.nat_embedding _ n).2),
+  exact hmn.ne ((hi.nat_embedding _).injective $ subtype.val_injective $
+    ha.eq_of_related (hi.nat_embedding _ m).2 (hi.nat_embedding _ n).2 h),
+end
+
+lemma finite.partially_well_ordered_on {s : set α} {r : α → α → Prop} [is_refl α r]
+  (hs : s.finite) :
+  s.partially_well_ordered_on r :=
+begin
+  intros f hf,
+  obtain ⟨m, n, hmn, h⟩ := hs.exists_lt_map_eq_of_range_subset hf,
+  exact ⟨m, n, hmn, h.subst $ refl (f m)⟩,
+end
+
+lemma _root_.is_antichain.partially_well_ordered_on_iff {s : set α} {r : α → α → Prop} [is_refl α r]
+  (hs : is_antichain r s) :
+  s.partially_well_ordered_on r ↔ s.finite :=
+⟨hs.finite_of_partially_well_ordered_on, finite.partially_well_ordered_on⟩
+
+lemma partially_well_ordered_on_iff_finite_antichains {s : set α} {r : α → α → Prop} [is_refl α r]
+  [is_symm α r] :
+  s.partially_well_ordered_on r ↔ ∀ t ⊆ s, is_antichain r t → t.finite :=
+begin
+  refine ⟨λ h t ht hrt, hrt.finite_of_partially_well_ordered_on (h.mono ht), _⟩,
+  rintro hs f hf,
+  by_contra' H,
+  refine set.infinite_range_of_injective (λ m n hmn, _) (hs _ hf _),
+  { obtain h | h | h := lt_trichotomy m n,
+    { refine (H _ _ h _).elim,
+      rw hmn,
+      exact refl _ },
+    { exact h },
+    { refine (H _ _ h _).elim,
+      rw hmn,
+      exact refl _ } },
+  rintro _ ⟨m, hm, rfl⟩ _ ⟨n, hn, rfl⟩ hmn,
+  obtain h | h  := (ne_of_apply_ne _ hmn).lt_or_lt,
+  { exact H _ _ h },
+  { exact mt symm (H _ _ h) }
+end
+
 section partial_order
 variables {s : set α} {t : set α} {r : α → α → Prop}
 
@@ -350,22 +401,9 @@ end set
 
 namespace finset
 
-@[simp]
-theorem partially_well_ordered_on {r : α → α → Prop} [is_refl α r] (f : finset α) :
-  set.partially_well_ordered_on (↑f : set α) r :=
-begin
-  intros g hg,
-  by_cases hinj : function.injective g,
-  { exact (set.infinite_of_injective_forall_mem hinj (set.range_subset_iff.1 hg)
-      f.finite_to_set).elim },
-  { rw [function.injective] at hinj,
-    push_neg at hinj,
-    obtain ⟨m, n, gmgn, hne⟩ := hinj,
-    cases lt_or_gt_of_ne hne with hlt hlt;
-    { refine ⟨_, _, hlt, _⟩,
-      rw gmgn,
-      exact refl_of r _, } }
-end
+@[simp] lemma partially_well_ordered_on {r : α → α → Prop} [is_refl α r] (s : finset α) :
+  (s : set α).partially_well_ordered_on r :=
+s.finite_to_set.partially_well_ordered_on
 
 @[simp]
 theorem is_pwo [partial_order α] (f : finset α) :