case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ (#R[X]) ≤ max (#R) ℵ₀

case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ (#R[X]) ≤ max (#R) ℵ₀
R : Type u
inst✝ : Semiring R
⊢ (#R[X]) ≤ max (#R) ℵ₀
cases subsingleton_or_nontrivial R
no goals
case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ (#R[X]) ≤ max (#R) ℵ₀
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
no goals
case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ (#R[X]) ≤ max (#R) ℵ₀
exact cardinal_mk_eq_max.le