case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ (#List α) = max (#α) ℵ₀

case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ (#List α) = max (#α) ℵ₀
α : Type u
inst✝ : Nonempty α
⊢ (#List α) = max (#α) ℵ₀
cases finite_or_infinite α
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ (#α) ≤ ℵ₀
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ (#List α) = max (#α) ℵ₀
rw [mk_list_eq_aleph0, eq_comm, max_eq_right]
no goals
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ (#α) ≤ ℵ₀
exact mk_le_aleph0
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ ℵ₀ ≤ (#α)
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ (#List α) = max (#α) ℵ₀
rw [mk_list_eq_mk, eq_comm, max_eq_left]
no goals
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ ℵ₀ ≤ (#α)
exact aleph0_le_mk α