α β : Type u
c : Cardinal
h : IsLimit c
h' : c < ℵ₀
⊢ False
α β : Type u
c : Cardinal
h : IsLimit c
⊢ ℵ₀ ≤ c
by_contra' h'
case intro.zero
α β : Type u
h : IsLimit ↑Nat.zero
h' : ↑Nat.zero < ℵ₀
⊢ False

case intro.succ
α β : Type u
n : ℕ
h : IsLimit ↑(Nat.succ n)
h' : ↑(Nat.succ n) < ℵ₀
⊢ False
α β : Type u
c : Cardinal
h : IsLimit c
h' : c < ℵ₀
⊢ False
rcases lt_aleph0.1 h' with ⟨_ | n, rfl⟩
no goals
case intro.zero
α β : Type u
h : IsLimit ↑Nat.zero
h' : ↑Nat.zero < ℵ₀
⊢ False
exact h.ne_zero.irrefl
case intro.succ
α β : Type u
n : ℕ
h : IsLimit (succ ↑n)
h' : ↑(Nat.succ n) < ℵ₀
⊢ False
case intro.succ
α β : Type u
n : ℕ
h : IsLimit ↑(Nat.succ n)
h' : ↑(Nat.succ n) < ℵ₀
⊢ False
rw [nat_succ] at h
no goals
case intro.succ
α β : Type u
n : ℕ
h : IsLimit (succ ↑n)
h' : ↑(Nat.succ n) < ℵ₀
⊢ False
exact not_isSuccLimit_succ _ h.isSuccLimit