feat: port #18526 (#3207)

Mathlib 3: https://github.com/leanprover-community/mathlib/pull/18526/files



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Order/Antisymmetrization.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module order.antisymmetrization
-! leanprover-community/mathlib commit f1a2caaf51ef593799107fe9a8d5e411599f3996
+! leanprover-community/mathlib commit 3353f661228bd27f632c600cd1a58b874d847c90
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -161,18 +161,12 @@ theorem antisymmetrization_fibration :
 
 theorem acc_antisymmetrization_iff : Acc (· < ·)
     (@toAntisymmetrization α (· ≤ ·) _ a) ↔ Acc (· < ·) a :=
-  ⟨fun h =>
-    haveI := InvImage.accessible _ h
-    this,
-    Acc.of_fibration _ antisymmetrization_fibration⟩
+  acc_liftOn₂'_iff
 #align acc_antisymmetrization_iff acc_antisymmetrization_iff
 
 theorem wellFounded_antisymmetrization_iff :
     WellFounded (@LT.lt (Antisymmetrization α (· ≤ ·)) _) ↔ WellFounded (@LT.lt α _) :=
-  ⟨fun h => ⟨fun a => acc_antisymmetrization_iff.1 <| h.apply _⟩, fun h =>
-    ⟨by
-      rintro ⟨a⟩
-      exact acc_antisymmetrization_iff.2 (h.apply a)⟩⟩
+  wellFounded_liftOn₂'_iff
 #align well_founded_antisymmetrization_iff wellFounded_antisymmetrization_iff
 
 instance [WellFoundedLT α] : WellFoundedLT (Antisymmetrization α (· ≤ ·)) :=
@@ -199,16 +193,14 @@ theorem toAntisymmetrization_lt_toAntisymmetrization_iff :
 
 @[simp]
 theorem ofAntisymmetrization_le_ofAntisymmetrization_iff {a b : Antisymmetrization α (· ≤ ·)} :
-    ofAntisymmetrization (· ≤ ·) a ≤ ofAntisymmetrization (· ≤ ·) b ↔ a ≤ b := by
-  rw [← toAntisymmetrization_le_toAntisymmetrization_iff]
-  simp
+    ofAntisymmetrization (· ≤ ·) a ≤ ofAntisymmetrization (· ≤ ·) b ↔ a ≤ b :=
+  (Quotient.out'RelEmbedding _).map_rel_iff
 #align of_antisymmetrization_le_of_antisymmetrization_iff ofAntisymmetrization_le_ofAntisymmetrization_iff
 
 @[simp]
 theorem ofAntisymmetrization_lt_ofAntisymmetrization_iff {a b : Antisymmetrization α (· ≤ ·)} :
-    ofAntisymmetrization (· ≤ ·) a < ofAntisymmetrization (· ≤ ·) b ↔ a < b := by
-  rw [← toAntisymmetrization_lt_toAntisymmetrization_iff]
-  simp
+    ofAntisymmetrization (· ≤ ·) a < ofAntisymmetrization (· ≤ ·) b ↔ a < b :=
+  (Quotient.out'RelEmbedding _).map_rel_iff
 #align of_antisymmetrization_lt_of_antisymmetrization_iff ofAntisymmetrization_lt_ofAntisymmetrization_iff
 
 @[mono]
@@ -250,10 +242,8 @@ variable (α)
 
 /-- `ofAntisymmetrization` as an order embedding. -/
 @[simps]
-noncomputable def OrderEmbedding.ofAntisymmetrization : Antisymmetrization α (· ≤ ·) ↪o α where
-  toFun := _root_.ofAntisymmetrization (. ≤ .)
-  inj' _ _ := Quotient.out_inj.1
-  map_rel_iff' := ofAntisymmetrization_le_ofAntisymmetrization_iff
+noncomputable def OrderEmbedding.ofAntisymmetrization : Antisymmetrization α (· ≤ ·) ↪o α :=
+  { Quotient.out'RelEmbedding _ with toFun := _root_.ofAntisymmetrization _ }
 #align order_embedding.of_antisymmetrization OrderEmbedding.ofAntisymmetrization
 #align order_embedding.of_antisymmetrization_apply OrderEmbedding.ofAntisymmetrization_apply
 

Mathlib/Order/RelIso/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module order.rel_iso.basic
-! leanprover-community/mathlib commit 76171581280d5b5d1e2d1f4f37e5420357bdc636
+! leanprover-community/mathlib commit 3353f661228bd27f632c600cd1a58b874d847c90
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -393,32 +393,79 @@ protected theorem isWellOrder : ∀ (_ : r ↪r s) [IsWellOrder β s], IsWellOrd
   | f, H => { f.isStrictTotalOrder with wf := f.wellFounded H.wf }
 #align rel_embedding.is_well_order RelEmbedding.isWellOrder
 
+/-- `quotient.mk` as a relation homomorphism between the relation and the lift of a relation. -/
+@[simps]
+def _root_.Quotient.mkRelHom [Setoid α] {r : α → α → Prop}
+    (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) : r →r Quotient.lift₂ r H :=
+  ⟨@Quotient.mk' α _, id⟩
+#align quotient.mk_rel_hom Quotient.mkRelHom
+
 /-- `Quotient.out` as a relation embedding between the lift of a relation and the relation. -/
 @[simps!]
-noncomputable def _root_.Quotient.outRelEmbedding [s : Setoid α] {r : α → α → Prop}
+noncomputable def _root_.Quotient.outRelEmbedding [Setoid α] {r : α → α → Prop}
     (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) : Quotient.lift₂ r H ↪r r :=
   ⟨Embedding.quotientOut α, by
     refine' @fun x y => Quotient.inductionOn₂ x y fun a b => _
     apply iff_iff_eq.2 (H _ _ _ _ _ _) <;> apply Quotient.mk_out⟩
 #align quotient.out_rel_embedding Quotient.outRelEmbedding
 #align quotient.out_rel_embedding_apply Quotient.outRelEmbedding_apply
 
+/-- `Quotient.out'` as a relation embedding between the lift of a relation and the relation. -/
+@[simps]
+noncomputable def _root_.Quotient.out'RelEmbedding {_ : Setoid α} {r : α → α → Prop}
+    (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) :
+    (fun a b => Quotient.liftOn₂' a b r H) ↪r r :=
+  { Quotient.outRelEmbedding _ with toFun := Quotient.out' }
+#align rel_embedding.quotient.out'_rel_embedding Quotient.out'RelEmbedding
+
+@[simp]
+theorem _root_.acc_lift₂_iff [Setoid α] {r : α → α → Prop}
+    {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} {a} :
+    Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a := by
+  constructor
+  · exact RelHomClass.acc (Quotient.mkRelHom H) a
+  · intro ac
+    induction' ac with _ _ IH
+    dsimp at IH
+    refine' ⟨_, fun q h => _⟩
+    obtain ⟨a', rfl⟩ := q.exists_rep
+    exact IH a' h
+#align acc_lift₂_iff acc_lift₂_iff
+
+@[simp]
+theorem _root_.acc_liftOn₂'_iff {s : Setoid α} {r : α → α → Prop} {H} {a} :
+    Acc (fun x y => Quotient.liftOn₂' x y r H) (Quotient.mk'' a : Quotient s) ↔ Acc r a :=
+  acc_lift₂_iff
+#align acc_lift_on₂'_iff acc_liftOn₂'_iff
+
 /-- A relation is well founded iff its lift to a quotient is. -/
 @[simp]
-theorem _root_.wellFounded_lift₂_iff [s : Setoid α] {r : α → α → Prop}
+theorem _root_.wellFounded_lift₂_iff [Setoid α] {r : α → α → Prop}
     {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} :
     WellFounded (Quotient.lift₂ r H) ↔ WellFounded r :=
-  ⟨fun hr => by
-    suffices ∀ {x : Quotient s} {a : α}, ⟦a⟧ = x → Acc r a by exact ⟨fun a => this rfl⟩
-    · refine' @fun x => @WellFounded.induction _ _ hr
-         (fun y => ∀ (a : α), Quotient.mk s a = y → Acc r a) x _
-      rintro x IH a rfl
-      exact ⟨_, @fun b hb => IH ⟦b⟧ hb _ rfl⟩
-      ,
-    (Quotient.outRelEmbedding H).wellFounded⟩
+  by
+  constructor
+  · exact RelHomClass.wellFounded (Quotient.mkRelHom H)
+  · refine' fun wf => ⟨fun q => _⟩
+    obtain ⟨a, rfl⟩ := q.exists_rep
+    exact acc_lift₂_iff.2 (wf.apply a)
 #align well_founded_lift₂_iff wellFounded_lift₂_iff
 
-alias wellFounded_lift₂_iff ↔ _root_.WellFounded.of_quotient_lift₂ _root_.WellFounded.quotient_lift₂
+alias _root_.wellFounded_lift₂_iff ↔
+  _root_.WellFounded.of_quotient_lift₂ _root_.WellFounded.quotient_lift₂
+#align well_founded.of_quotient_lift₂ WellFounded.of_quotient_lift₂
+#align well_founded.quotient_lift₂ WellFounded.quotient_lift₂
+
+@[simp]
+theorem _root_.wellFounded_liftOn₂'_iff {s : Setoid α} {r : α → α → Prop} {H} :
+    (WellFounded fun x y : Quotient s => Quotient.liftOn₂' x y r H) ↔ WellFounded r :=
+  wellFounded_lift₂_iff
+#align well_founded_lift_on₂'_iff wellFounded_liftOn₂'_iff
+
+alias _root_.wellFounded_liftOn₂'_iff ↔
+  _root_.WellFounded.of_quotient_liftOn₂' _root_.WellFounded.quotient_liftOn₂'
+#align well_founded.of_quotient_lift_on₂' WellFounded.of_quotient_liftOn₂'
+#align well_founded.quotient_lift_on₂' WellFounded.quotient_liftOn₂'
 
 /-- To define an relation embedding from an antisymmetric relation `r` to a reflexive relation `s`
 it suffices to give a function together with a proof that it satisfies `s (f a) (f b) ↔ r a b`.