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

case inr
α : Type u
h✝ : Infinite α
⊢ (#List α) ≤ max ℵ₀ (#α)
α : Type u
⊢ (#List α) ≤ max ℵ₀ (#α)
cases finite_or_infinite α
no goals
case inl
α : Type u
h✝ : Finite α
⊢ (#List α) ≤ max ℵ₀ (#α)
exact mk_le_aleph0.trans (le_max_left _ _)
case inr
α : Type u
h✝ : Infinite α
⊢ (#α) ≤ max ℵ₀ (#α)
case inr
α : Type u
h✝ : Infinite α
⊢ (#List α) ≤ max ℵ₀ (#α)
rw [mk_list_eq_mk]
no goals
case inr
α : Type u
h✝ : Infinite α
⊢ (#α) ≤ max ℵ₀ (#α)
apply le_max_right