case intro
α✝ β α : Type u
h : (#α) = ℵ₀
f : α ≃ ULift ℕ
⊢ Nonempty (Denumerable α)
α✝ β α : Type u
h : (#α) = ℵ₀
⊢ Nonempty (Denumerable α)
cases' Quotient.exact h with f
no goals
case intro
α✝ β α : Type u
h : (#α) = ℵ₀
f : α ≃ ULift ℕ
⊢ Nonempty (Denumerable α)
exact ⟨Denumerable.mk' <| f.trans Equiv.ulift⟩