α β : Type u
n : ℕ
⊢ Nonempty (Fin (Nat.succ n) ↪ ℕ)
α β : Type u
n : ℕ
⊢ succ ↑n ≤ ℵ₀
rw [← nat_succ, ← lift_mk_fin, aleph0, lift_mk_le.{0, 0, u}]
no goals
α β : Type u
n : ℕ
⊢ Nonempty (Fin (Nat.succ n) ↪ ℕ)
exact ⟨⟨(↑), fun a b => Fin.ext⟩⟩