case intro
α β : Type u
n : ℕ
h : ∀ (n_1 : ℕ), ↑n_1 ≤ ↑n
hn : ↑n < ℵ₀
⊢ False
α β : Type u
c : Cardinal
h : ∀ (n : ℕ), ↑n ≤ c
hn : c < ℵ₀
⊢ False
rcases lt_aleph0.1 hn with ⟨n, rfl⟩
no goals
case intro
α β : Type u
n : ℕ
h : ∀ (n_1 : ℕ), ↑n_1 ≤ ↑n
hn : ↑n < ℵ₀
⊢ False
exact (Nat.lt_succ_self _).not_le (natCast_le.1 (h (n + 1)))