From 522ace495538604270b08649e9aee5a226f20eae Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxumath@gmail.com>
Date: Tue, 4 Oct 2022 05:52:16 +0000
Subject: [PATCH] feat(order/antisymmetrization): (<) is well-founded for a
 preorder iff well-founded on its antisymmetrization (#16741)

+ Show that the antisymmetrization of a well-founded preorder is a well-founded partial order. Useful for reducing well-foundedness of preorders to partial orders.

+ fix reference to renamed lemma `well_founded.prod_game_add` in docstring.
---
 src/order/antisymmetrization.lean | 17 +++++++++++++++++
 src/order/game_add.lean           |  4 ++--
 2 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/src/order/antisymmetrization.lean b/src/order/antisymmetrization.lean
index 4e8098fb5a811..ca73c3d0b8a09 100644
--- a/src/order/antisymmetrization.lean
+++ b/src/order/antisymmetrization.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import order.hom.basic
+import logic.relation
 
 /-!
 # Turning a preorder into a partial order
@@ -108,6 +109,22 @@ instance : partial_order (antisymmetrization α (≤)) :=
   lt_iff_le_not_le := λ a b, quotient.induction_on₂' a b $ λ a b, lt_iff_le_not_le,
   le_antisymm := λ a b, quotient.induction_on₂' a b $ λ a b hab hba, quotient.sound' ⟨hab, hba⟩ }
 
+lemma antisymmetrization_fibration :
+  relation.fibration (<) (<) (@to_antisymmetrization α (≤) _) :=
+by { rintro a ⟨b⟩ h, exact ⟨b, h, rfl⟩ }
+
+lemma acc_antisymmetrization_iff : acc (<) (to_antisymmetrization (≤) a) ↔ acc (<) a :=
+⟨λ h, by { have := inv_image.accessible _ h, exact this },
+  acc.of_fibration _ antisymmetrization_fibration⟩
+
+lemma well_founded_antisymmetrization_iff :
+  well_founded (@has_lt.lt (antisymmetrization α (≤)) _) ↔ well_founded (@has_lt.lt α _) :=
+⟨λ h, ⟨λ a, acc_antisymmetrization_iff.1 $ h.apply _⟩,
+  λ h, ⟨by { rintro ⟨a⟩, exact acc_antisymmetrization_iff.2 (h.apply a) }⟩⟩
+
+instance [well_founded_lt α] : well_founded_lt (antisymmetrization α (≤)) :=
+⟨well_founded_antisymmetrization_iff.2 is_well_founded.wf⟩
+
 instance [@decidable_rel α (≤)] [@decidable_rel α (<)] [is_total α (≤)] :
   linear_order (antisymmetrization α (≤)) :=
 { le_total := λ a b, quotient.induction_on₂' a b $ total_of (≤),
diff --git a/src/order/game_add.lean b/src/order/game_add.lean
index c72282c7729f9..8bc7d3cc51ee8 100644
--- a/src/order/game_add.lean
+++ b/src/order/game_add.lean
@@ -18,8 +18,8 @@ subsequency relation on the addition of combinatorial games.
 ## Main definitions and results
 
 - `prod.game_add`: the game addition relation on ordered pairs.
-- `well_founded.game_add`: formalizes induction on ordered pairs, where exactly one entry decreases
-  at a time.
+- `well_founded.prod_game_add`: formalizes induction on ordered pairs, where exactly one entry
+  decreases at a time.
 
 ## Todo