case inl
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ (#MvPolynomial σ R) ≤ max (max (lift (#R)) (lift (#σ))) ℵ₀

case inr
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (#MvPolynomial σ R) ≤ max (max (lift (#R)) (lift (#σ))) ℵ₀
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ (#MvPolynomial σ R) ≤ max (max (lift (#R)) (lift (#σ))) ℵ₀
cases subsingleton_or_nontrivial R
case inr.inl
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : IsEmpty σ
⊢ (#MvPolynomial σ R) ≤ max (max (lift (#R)) (lift (#σ))) ℵ₀

case inr.inr
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : Nonempty σ
⊢ (#MvPolynomial σ R) ≤ max (max (lift (#R)) (lift (#σ))) ℵ₀
case inr
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (#MvPolynomial σ R) ≤ max (max (lift (#R)) (lift (#σ))) ℵ₀
cases isEmpty_or_nonempty σ
no goals
case inl
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ (#MvPolynomial σ R) ≤ max (max (lift (#R)) (lift (#σ))) ℵ₀
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
no goals
case inr.inl
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : IsEmpty σ
⊢ (#MvPolynomial σ R) ≤ max (max (lift (#R)) (lift (#σ))) ℵ₀
exact cardinal_mk_eq_lift.trans_le (le_max_of_le_left <| le_max_left _ _)
no goals
case inr.inr
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : Nonempty σ
⊢ (#MvPolynomial σ R) ≤ max (max (lift (#R)) (lift (#σ))) ℵ₀
exact cardinal_mk_eq_max_lift.le