From 5bb7551416b28f2800f1611c1ac6ae91fb37d87c Mon Sep 17 00:00:00 2001
From: staroperator <staroperator92@gmail.com>
Date: Wed, 21 Jan 2026 22:02:14 -0500
Subject: [PATCH 1/7] add

---
 Mathlib/Data/Set/Countable.lean | 67 +++++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)

diff --git a/Mathlib/Data/Set/Countable.lean b/Mathlib/Data/Set/Countable.lean
index e469971767251e..aad1a1a1a1015e 100644
--- a/Mathlib/Data/Set/Countable.lean
+++ b/Mathlib/Data/Set/Countable.lean
@@ -321,3 +321,70 @@ end Set
 
 theorem Finset.countable_toSet (s : Finset α) : Set.Countable (↑s : Set α) :=
   s.finite_toSet.countable
+
+namespace Set
+
+/-- A set is uncountable if it is not countable.
+
+This is protected so that it does not conflict with global `Uncountable`. -/
+protected def Uncountable (s : Set α) : Prop :=
+  ¬s.Countable
+
+@[simp, push]
+theorem not_countable_iff_uncountable {s : Set α} : ¬s.Countable ↔ s.Uncountable := .rfl
+
+@[simp, push]
+theorem not_uncountable_iff_countable {s : Set α} : ¬s.Uncountable ↔ s.Countable :=
+  not_not
+
+alias ⟨_, Countable.not_uncountable⟩ := not_uncountable_iff_countable
+
+@[simp] lemma Uncountable.not_countable {s : Set α} (hs : s.Uncountable) : ¬ s.Countable := hs
+
+attribute [simp] Countable.not_uncountable
+
+theorem uncountable_coe_iff {s : Set α} : Uncountable s ↔ s.Uncountable :=
+  not_countable_iff.symm.trans countable_coe_iff.not
+
+alias ⟨_root_.Uncountable.to_set, Uncountable.to_subtype⟩ := uncountable_coe_iff
+
+theorem uncountable_univ_iff : (@univ α).Uncountable ↔ Uncountable α := by
+  rw [Set.Uncountable, countable_univ_iff, not_countable_iff]
+
+theorem uncountable_univ [h : Uncountable α] : (@univ α).Uncountable :=
+  uncountable_univ_iff.2 h
+
+theorem uncountable_of_countable_compl [Uncountable α] {s : Set α} (hs : sᶜ.Countable) :
+    s.Uncountable := fun h =>
+  Set.uncountable_univ (α := α) (by simpa using hs.union h)
+
+theorem Finite.uncountable_compl [Uncountable α] {s : Set α} (hs : s.Countable) :
+    sᶜ.Uncountable := fun h =>
+  Set.uncountable_univ (α := α) (by simpa using hs.union h)
+
+theorem Uncountable.diff {s t : Set α} (hs : s.Uncountable) (ht : t.Countable) :
+    (s \ t).Uncountable := fun h =>
+  hs <| h.of_diff ht
+
+@[simp]
+theorem uncountable_union {s t : Set α} : (s ∪ t).Uncountable ↔ s.Uncountable ∨ t.Uncountable := by
+  simp only [Set.Uncountable, countable_union, not_and_or]
+
+theorem Uncountable.of_image (f : α → β) {s : Set α} (hs : (f '' s).Uncountable) : s.Uncountable :=
+  mt (Countable.image · f) hs
+
+theorem Uncountable.image {s : Set α} {f : α → β} (hs : s.Uncountable) (hi : InjOn f s) :
+    (f '' s).Uncountable :=
+  mt (countable_of_injective_of_countable_image hi) hs
+
+theorem Uncountable.range [Uncountable α] {f : α → β} (hi : Injective f) :
+    (range f).Uncountable := by
+  simpa using uncountable_univ.image (hi.injOn (s := Set.univ))
+
+theorem Uncountable.infinite {s : Set α} (hs : s.Uncountable) : s.Infinite :=
+  mt Finite.countable hs
+
+theorem Uncountable.nonempty {s : Set α} (hs : s.Uncountable) : s.Nonempty :=
+  hs.infinite.nonempty
+
+end Set

From 0cd051a1337bbd4466763de09273895ac62333e8 Mon Sep 17 00:00:00 2001
From: staroperator <staroperator92@gmail.com>
Date: Wed, 21 Jan 2026 22:49:32 -0500
Subject: [PATCH 2/7] fix

---
 Mathlib/Analysis/Real/Cardinality.lean | 8 ++++----
 Mathlib/SetTheory/Cardinal/Basic.lean  | 5 +++++
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Real/Cardinality.lean b/Mathlib/Analysis/Real/Cardinality.lean
index 7286396fa4e0cf..376c29d476d9ca 100644
--- a/Mathlib/Analysis/Real/Cardinality.lean
+++ b/Mathlib/Analysis/Real/Cardinality.lean
@@ -268,7 +268,7 @@ lemma Real.Ioo_countable_iff {x y : ℝ} :
     (Ioo x y).Countable ↔ y ≤ x := by
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
   contrapose! h
-  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real h, not_le]
+  rw [← Cardinal.aleph0_lt_iff_set_uncountable, Cardinal.mk_Ioo_real h]
   exact Cardinal.aleph0_lt_continuum
 
 @[simp]
@@ -276,7 +276,7 @@ lemma Real.Ico_countable_iff {x y : ℝ} :
     (Ico x y).Countable ↔ y ≤ x := by
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
   contrapose! h
-  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ico_real h, not_le]
+  rw [← Cardinal.aleph0_lt_iff_set_uncountable, Cardinal.mk_Ico_real h]
   exact Cardinal.aleph0_lt_continuum
 
 @[simp]
@@ -284,7 +284,7 @@ lemma Real.Ioc_countable_iff {x y : ℝ} :
     (Ioc x y).Countable ↔ y ≤ x := by
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
   contrapose! h
-  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioc_real h, not_le]
+  rw [← Cardinal.aleph0_lt_iff_set_uncountable, Cardinal.mk_Ioc_real h]
   exact Cardinal.aleph0_lt_continuum
 
 @[simp]
@@ -295,7 +295,7 @@ lemma Real.Icc_countable_iff {x y : ℝ} :
     · simp [heq]
     · simp [hlt]⟩
   contrapose! h
-  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Icc_real h, not_le]
+  rw [← Cardinal.aleph0_lt_iff_set_uncountable, Cardinal.mk_Icc_real h]
   exact Cardinal.aleph0_lt_continuum
 
 end Cardinal
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index 2e1510cad20e8e..105eee980aa13f 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -443,6 +443,11 @@ theorem aleph0_lt_mk_iff : ℵ₀ < #α ↔ Uncountable α := by
 theorem aleph0_lt_mk [Uncountable α] : ℵ₀ < #α :=
   aleph0_lt_mk_iff.mpr ‹_›
 
+theorem aleph0_lt_iff_set_uncountable {s : Set α} : ℵ₀ < #s ↔ s.Uncountable :=
+  aleph0_lt_mk_iff.trans uncountable_coe_iff
+
+alias ⟨_, _root_.Set.Uncountable.aleph0_lt⟩ := aleph0_lt_iff_set_uncountable
+
 instance canLiftCardinalNat : CanLift Cardinal ℕ (↑) fun x => x < ℵ₀ :=
   ⟨fun _ hx =>
     let ⟨n, hn⟩ := lt_aleph0.mp hx

From c89b4b80b264c39decfbd77aaa3bfe21e9c340e1 Mon Sep 17 00:00:00 2001
From: staroperator <staroperator92@gmail.com>
Date: Wed, 21 Jan 2026 22:56:00 -0500
Subject: [PATCH 3/7] add nontrivial

---
 Mathlib/Data/Set/Countable.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Data/Set/Countable.lean b/Mathlib/Data/Set/Countable.lean
index aad1a1a1a1015e..1b38752d0b1c90 100644
--- a/Mathlib/Data/Set/Countable.lean
+++ b/Mathlib/Data/Set/Countable.lean
@@ -387,4 +387,7 @@ theorem Uncountable.infinite {s : Set α} (hs : s.Uncountable) : s.Infinite :=
 theorem Uncountable.nonempty {s : Set α} (hs : s.Uncountable) : s.Nonempty :=
   hs.infinite.nonempty
 
+theorem Uncountable.nontrivial {s : Set α} (hs : s.Uncountable) : s.Nontrivial :=
+  hs.infinite.nontrivial
+
 end Set

From 98f778c54fa9cab5f2148c52e10cb9aa67f5037b Mon Sep 17 00:00:00 2001
From: staroperator <staroperator92@gmail.com>
Date: Wed, 21 Jan 2026 23:23:02 -0500
Subject: [PATCH 4/7] add mono

---
 Mathlib/Data/Set/Countable.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Data/Set/Countable.lean b/Mathlib/Data/Set/Countable.lean
index 1b38752d0b1c90..aa7fc7f66f4d70 100644
--- a/Mathlib/Data/Set/Countable.lean
+++ b/Mathlib/Data/Set/Countable.lean
@@ -354,6 +354,9 @@ theorem uncountable_univ_iff : (@univ α).Uncountable ↔ Uncountable α := by
 theorem uncountable_univ [h : Uncountable α] : (@univ α).Uncountable :=
   uncountable_univ_iff.2 h
 
+protected lemma Uncountable.mono {s t : Set α} (h : s ⊆ t) : s.Uncountable → t.Uncountable :=
+  mt (·.mono h)
+
 theorem uncountable_of_countable_compl [Uncountable α] {s : Set α} (hs : sᶜ.Countable) :
     s.Uncountable := fun h =>
   Set.uncountable_univ (α := α) (by simpa using hs.union h)

From a654426e3d4f5bf70ab77b973e976e9fb603ace9 Mon Sep 17 00:00:00 2001
From: staroperator <staroperator92@gmail.com>
Date: Thu, 22 Jan 2026 00:25:11 -0500
Subject: [PATCH 5/7] fix name

---
 Mathlib/Data/Set/Countable.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Set/Countable.lean b/Mathlib/Data/Set/Countable.lean
index aa7fc7f66f4d70..bc49495d50d306 100644
--- a/Mathlib/Data/Set/Countable.lean
+++ b/Mathlib/Data/Set/Countable.lean
@@ -361,7 +361,7 @@ theorem uncountable_of_countable_compl [Uncountable α] {s : Set α} (hs : sᶜ.
     s.Uncountable := fun h =>
   Set.uncountable_univ (α := α) (by simpa using hs.union h)
 
-theorem Finite.uncountable_compl [Uncountable α] {s : Set α} (hs : s.Countable) :
+theorem Countable.uncountable_compl [Uncountable α] {s : Set α} (hs : s.Countable) :
     sᶜ.Uncountable := fun h =>
   Set.uncountable_univ (α := α) (by simpa using hs.union h)
 

From b995b1fe887b294fa5694e696754765616a2351e Mon Sep 17 00:00:00 2001
From: staroperator <staroperator92@gmail.com>
Date: Fri, 30 Jan 2026 11:07:39 -0500
Subject: [PATCH 6/7] unsimp

---
 Mathlib/Data/Finite/Defs.lean   | 4 +---
 Mathlib/Data/Set/Countable.lean | 4 +---
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Finite/Defs.lean b/Mathlib/Data/Finite/Defs.lean
index 770945106f9770..92eb85e44f2f38 100644
--- a/Mathlib/Data/Finite/Defs.lean
+++ b/Mathlib/Data/Finite/Defs.lean
@@ -215,9 +215,7 @@ theorem not_infinite {s : Set α} : ¬s.Infinite ↔ s.Finite :=
 
 alias ⟨_, Finite.not_infinite⟩ := not_infinite
 
-@[simp] lemma Infinite.not_finite {s : Set α} (hs : s.Infinite) : ¬ s.Finite := hs
-
-attribute [simp] Finite.not_infinite
+lemma Infinite.not_finite {s : Set α} (hs : s.Infinite) : ¬ s.Finite := hs
 
 /-- See also `finite_or_infinite`, `fintypeOrInfinite`. -/
 protected theorem finite_or_infinite (s : Set α) : s.Finite ∨ s.Infinite :=
diff --git a/Mathlib/Data/Set/Countable.lean b/Mathlib/Data/Set/Countable.lean
index bc49495d50d306..0a3c49ade6b393 100644
--- a/Mathlib/Data/Set/Countable.lean
+++ b/Mathlib/Data/Set/Countable.lean
@@ -339,9 +339,7 @@ theorem not_uncountable_iff_countable {s : Set α} : ¬s.Uncountable ↔ s.Count
 
 alias ⟨_, Countable.not_uncountable⟩ := not_uncountable_iff_countable
 
-@[simp] lemma Uncountable.not_countable {s : Set α} (hs : s.Uncountable) : ¬ s.Countable := hs
-
-attribute [simp] Countable.not_uncountable
+lemma Uncountable.not_countable {s : Set α} (hs : s.Uncountable) : ¬ s.Countable := hs
 
 theorem uncountable_coe_iff {s : Set α} : Uncountable s ↔ s.Uncountable :=
   not_countable_iff.symm.trans countable_coe_iff.not

From 68e89e0edf883b53e5fdb0855d9ecce1accbada6 Mon Sep 17 00:00:00 2001
From: staroperator <staroperator92@gmail.com>
Date: Fri, 30 Jan 2026 14:02:16 -0500
Subject: [PATCH 7/7] Revert "unsimp"

This reverts commit b995b1fe887b294fa5694e696754765616a2351e.
---
 Mathlib/Data/Finite/Defs.lean   | 4 +++-
 Mathlib/Data/Set/Countable.lean | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Finite/Defs.lean b/Mathlib/Data/Finite/Defs.lean
index 92eb85e44f2f38..770945106f9770 100644
--- a/Mathlib/Data/Finite/Defs.lean
+++ b/Mathlib/Data/Finite/Defs.lean
@@ -215,7 +215,9 @@ theorem not_infinite {s : Set α} : ¬s.Infinite ↔ s.Finite :=
 
 alias ⟨_, Finite.not_infinite⟩ := not_infinite
 
-lemma Infinite.not_finite {s : Set α} (hs : s.Infinite) : ¬ s.Finite := hs
+@[simp] lemma Infinite.not_finite {s : Set α} (hs : s.Infinite) : ¬ s.Finite := hs
+
+attribute [simp] Finite.not_infinite
 
 /-- See also `finite_or_infinite`, `fintypeOrInfinite`. -/
 protected theorem finite_or_infinite (s : Set α) : s.Finite ∨ s.Infinite :=
diff --git a/Mathlib/Data/Set/Countable.lean b/Mathlib/Data/Set/Countable.lean
index 0a3c49ade6b393..bc49495d50d306 100644
--- a/Mathlib/Data/Set/Countable.lean
+++ b/Mathlib/Data/Set/Countable.lean
@@ -339,7 +339,9 @@ theorem not_uncountable_iff_countable {s : Set α} : ¬s.Uncountable ↔ s.Count
 
 alias ⟨_, Countable.not_uncountable⟩ := not_uncountable_iff_countable
 
-lemma Uncountable.not_countable {s : Set α} (hs : s.Uncountable) : ¬ s.Countable := hs
+@[simp] lemma Uncountable.not_countable {s : Set α} (hs : s.Uncountable) : ¬ s.Countable := hs
+
+attribute [simp] Countable.not_uncountable
 
 theorem uncountable_coe_iff {s : Set α} : Uncountable s ↔ s.Uncountable :=
   not_countable_iff.symm.trans countable_coe_iff.not