case intro
α β : Type u
n : ℕ
ha : ↑n < ℵ₀
⊢ succ ↑n < ℵ₀
α β : Type u
a : Cardinal
ha : a < ℵ₀
⊢ succ a < ℵ₀
rcases lt_aleph0.1 ha with ⟨n, rfl⟩
case intro
α β : Type u
n : ℕ
ha : ↑n < ℵ₀
⊢ ↑(Nat.succ n) < ℵ₀
case intro
α β : Type u
n : ℕ
ha : ↑n < ℵ₀
⊢ succ ↑n < ℵ₀
rw [← nat_succ]
no goals
case intro
α β : Type u
n : ℕ
ha : ↑n < ℵ₀
⊢ ↑(Nat.succ n) < ℵ₀
apply nat_lt_aleph0