Theorem: not_countable_Ioo (Ray/Misc/TotallyDisconnected.lean)

State before:
a b : ℝ
h : a < b
⊢ ¬(Ioo a b).Countable
Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, not_le, Cardinal.mk_Ioo_real h]
State after:
a b : ℝ
h : a < b
⊢ Cardinal.aleph0 < Cardinal.continuum

State before:
a b : ℝ
h : a < b
⊢ Cardinal.aleph0 < Cardinal.continuum
Tactic:
apply Cardinal.cantor
State after:
no goals