fix

Author: staroperator

Mathlib/Analysis/Real/Cardinality.lean

@@ -268,23 +268,23 @@ 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]
 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]
 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

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