no goals
σ : Type u
R : Type v
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ max (lift (#σ →₀ ℕ)) (lift (#R)) = max (max (lift (#R)) (lift (#σ))) ℵ₀
rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph0, max_comm]