From b57c80c028094e8367b9dcc94f1c726a86bccf7e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 28 Apr 2023 14:30:45 +0000
Subject: [PATCH] feat: Lemmas relating definitions of infinite sets (#3672)

Match https://github.com/leanprover-community/mathlib/pull/18620

* [`data.set.finite`@`c941bb9426d62e266612b6d99e6c9fc93e7a1d07`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/finite?range=c941bb9426d62e266612b6d99e6c9fc93e7a1d07..52fa514ec337dd970d71d8de8d0fd68b455a1e54)
* [`data.finset.locally_finite`@`f24cc2891c0e328f0ee8c57387103aa462c44b5e`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/locally_finite?range=f24cc2891c0e328f0ee8c57387103aa462c44b5e..52fa514ec337dd970d71d8de8d0fd68b455a1e54)
* [`data.nat.lattice`@`2445c98ae4b87eabebdde552593519b9b6dc350c`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/lattice?range=2445c98ae4b87eabebdde552593519b9b6dc350c..52fa514ec337dd970d71d8de8d0fd68b455a1e54)
---
 Mathlib/Data/Finset/LocallyFinite.lean | 36 +++++++++++++++++++++++++-
 Mathlib/Data/Nat/Lattice.lean          |  5 ++--
 Mathlib/Data/Set/Finite.lean           | 24 ++++++++++++-----
 3 files changed, 56 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Data/Finset/LocallyFinite.lean b/Mathlib/Data/Finset/LocallyFinite.lean
index 2672be49cbe586..2c3fe07e3bd6c4 100644
--- a/Mathlib/Data/Finset/LocallyFinite.lean
+++ b/Mathlib/Data/Finset/LocallyFinite.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Yaël Dillies
 
 ! This file was ported from Lean 3 source module data.finset.locally_finite
-! leanprover-community/mathlib commit f24cc2891c0e328f0ee8c57387103aa462c44b5e
+! leanprover-community/mathlib commit 52fa514ec337dd970d71d8de8d0fd68b455a1e54
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -464,6 +464,10 @@ theorem _root_.BddBelow.finite {s : Set α} (hs : BddBelow s) : s.Finite :=
   (Ici a).finite_toSet.subset fun _ hx => mem_Ici.2 <| ha hx
 #align bdd_below.finite BddBelow.finite
 
+theorem _root_.Set.Infinite.not_bddBelow {s : Set α} : s.Infinite → ¬BddBelow s :=
+  mt BddBelow.finite
+#align set.infinite.not_bdd_below Set.Infinite.not_bddBelow
+
 variable [Fintype α]
 
 theorem filter_lt_eq_Ioi [DecidablePred ((· < ·) a)] : univ.filter ((· < ·) a) = Ioi a := by
@@ -490,6 +494,10 @@ theorem _root_.BddAbove.finite {s : Set α} (hs : BddAbove s) : s.Finite :=
   hs.dual.finite
 #align bdd_above.finite BddAbove.finite
 
+theorem _root_.Set.Infinite.not_bddAbove {s : Set α} : s.Infinite → ¬BddAbove s :=
+  mt BddAbove.finite
+#align set.infinite.not_bdd_above Set.Infinite.not_bddAbove
+
 variable [Fintype α]
 
 theorem filter_gt_eq_Iio [DecidablePred (· < a)] : univ.filter (· < a) = Iio a := by
@@ -825,6 +833,32 @@ theorem Ico_diff_Ico_right (a b c : α) : Ico a b \ Ico c b = Ico a (min b c) :=
 
 end LocallyFiniteOrder
 
+section LocallyFiniteOrderBot
+variable [LocallyFiniteOrderBot α] {s : Set α}
+
+theorem _root_.Set.Infinite.exists_gt (hs : s.Infinite) : ∀ a, ∃ b ∈ s, a < b :=
+  not_bddAbove_iff.1 hs.not_bddAbove
+#align set.infinite.exists_gt Set.Infinite.exists_gt
+
+theorem _root_.Set.infinite_iff_exists_gt [Nonempty α] : s.Infinite ↔ ∀ a, ∃ b ∈ s, a < b :=
+  ⟨Set.Infinite.exists_gt, Set.infinite_of_forall_exists_gt⟩
+#align set.infinite_iff_exists_gt Set.infinite_iff_exists_gt
+
+end LocallyFiniteOrderBot
+
+section LocallyFiniteOrderTop
+variable [LocallyFiniteOrderTop α] {s : Set α}
+
+theorem _root_.Set.Infinite.exists_lt (hs : s.Infinite) : ∀ a, ∃ b ∈ s, b < a :=
+  not_bddBelow_iff.1 hs.not_bddBelow
+#align set.infinite.exists_lt Set.Infinite.exists_lt
+
+theorem _root_.Set.infinite_iff_exists_lt [Nonempty α] : s.Infinite ↔ ∀ a, ∃ b ∈ s, b < a :=
+  ⟨Set.Infinite.exists_lt, Set.infinite_of_forall_exists_lt⟩
+#align set.infinite_iff_exists_lt Set.infinite_iff_exists_lt
+
+end LocallyFiniteOrderTop
+
 variable [Fintype α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α]
 
 theorem Ioi_disjUnion_Iio (a : α) :
diff --git a/Mathlib/Data/Nat/Lattice.lean b/Mathlib/Data/Nat/Lattice.lean
index dbf7d0e75ef766..754cda36fcbdd4 100644
--- a/Mathlib/Data/Nat/Lattice.lean
+++ b/Mathlib/Data/Nat/Lattice.lean
@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Gabriel Ebner, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module data.nat.lattice
-! leanprover-community/mathlib commit 2445c98ae4b87eabebdde552593519b9b6dc350c
+! leanprover-community/mathlib commit 52fa514ec337dd970d71d8de8d0fd68b455a1e54
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
+import Mathlib.Data.Nat.Interval
 import Mathlib.Order.ConditionallyCompleteLattice.Finset
 
 /-!
@@ -43,7 +44,7 @@ theorem supₛ_def {s : Set ℕ} (h : ∃ n, ∀ a ∈ s, a ≤ n) :
 
 theorem _root_.Set.Infinite.Nat.supₛ_eq_zero {s : Set ℕ} (h : s.Infinite) : supₛ s = 0 :=
   dif_neg fun ⟨n, hn⟩ ↦
-    let ⟨k, hks, hk⟩ := h.exists_nat_lt n
+    let ⟨k, hks, hk⟩ := h.exists_gt n
     (hn k hks).not_lt hk
 #align set.infinite.nat.Sup_eq_zero Set.Infinite.Nat.supₛ_eq_zero
 
diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean
index 1b294f0488cce0..2f15a394a88dbb 100644
--- a/Mathlib/Data/Set/Finite.lean
+++ b/Mathlib/Data/Set/Finite.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kyle Miller
 
 ! This file was ported from Lean 3 source module data.set.finite
-! leanprover-community/mathlib commit c941bb9426d62e266612b6d99e6c9fc93e7a1d07
+! leanprover-community/mathlib commit 52fa514ec337dd970d71d8de8d0fd68b455a1e54
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1366,11 +1366,6 @@ theorem infinite_of_injective_forall_mem [Infinite α] {s : Set β} {f : α →
   exact (infinite_range_of_injective hi).mono hf
 #align set.infinite_of_injective_forall_mem Set.infinite_of_injective_forall_mem
 
-theorem Infinite.exists_nat_lt {s : Set ℕ} (hs : s.Infinite) (n : ℕ) : ∃ m ∈ s, n < m :=
-  let ⟨m, hm⟩ := (hs.diff <| Set.finite_le_nat n).nonempty
-  ⟨m, by simpa using hm⟩
-#align set.infinite.exists_nat_lt Set.Infinite.exists_nat_lt
-
 theorem Infinite.exists_not_mem_finset {s : Set α} (hs : s.Infinite) (f : Finset α) :
     ∃ a ∈ s, a ∉ f :=
   let ⟨a, has, haf⟩ := (hs.diff (toFinite f)).nonempty
@@ -1391,6 +1386,23 @@ theorem not_injOn_infinite_finite_image {f : α → β} {s : Set α} (h_inf : s.
 
 /-! ### Order properties -/
 
+section Preorder
+
+variable [Preorder α] [Nonempty α] {s : Set α}
+
+theorem infinite_of_forall_exists_gt (h : ∀ a, ∃ b ∈ s, a < b) : s.Infinite := by
+  inhabit α
+  set f : ℕ → α := fun n => Nat.recOn n (h default).choose fun n a => (h a).choose
+  have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1
+  exact infinite_of_injective_forall_mem
+    (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf
+#align set.infinite_of_forall_exists_gt Set.infinite_of_forall_exists_gt
+
+theorem infinite_of_forall_exists_lt (h : ∀ a, ∃ b ∈ s, b < a) : s.Infinite :=
+  @infinite_of_forall_exists_gt αᵒᵈ _ _ _ h
+#align set.infinite_of_forall_exists_lt Set.infinite_of_forall_exists_lt
+
+end Preorder
 
 theorem finite_isTop (α : Type _) [PartialOrder α] : { x : α | IsTop x }.Finite :=
   (subsingleton_isTop α).finite