[GOAL]
σ : Type u
R : Type v
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ max (lift #(σ →₀ ℕ)) (lift #R) = max (max (lift #R) (lift #σ)) ℵ₀
[PROOFSTEP]
rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph0, max_comm]
[GOAL]
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ #(MvPolynomial σ R) ≤ max (max (lift #R) (lift #σ)) ℵ₀
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
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 #σ)) ℵ₀
[PROOFSTEP]
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
[GOAL]
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 #σ)) ℵ₀
[PROOFSTEP]
cases isEmpty_or_nonempty σ
[GOAL]
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 #σ)) ℵ₀
[PROOFSTEP]
exact cardinal_mk_eq_lift.trans_le (le_max_of_le_left <| le_max_left _ _)
[GOAL]
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 #σ)) ℵ₀
[PROOFSTEP]
exact cardinal_mk_eq_max_lift.le
[GOAL]
σ R : Type u
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ #(MvPolynomial σ R) = max (max #R #σ) ℵ₀
[PROOFSTEP]
simp
[GOAL]
σ R : Type u
inst✝ : CommSemiring R
⊢ max (max (lift #R) (lift #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀
[PROOFSTEP]
rw [lift_id, lift_id]
