[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ #(AddMonoidAlgebra R ℕ) = max #R ℵ₀
[PROOFSTEP]
rw [AddMonoidAlgebra, mk_finsupp_lift_of_infinite, lift_uzero, max_comm]
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ max (#R) (lift #ℕ) = max #R ℵ₀
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Semiring R
⊢ #R[X] ≤ max #R ℵ₀
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ #R[X] ≤ max #R ℵ₀
[PROOFSTEP]
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
[GOAL]
case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀
[PROOFSTEP]
exact cardinal_mk_eq_max.le
