no goals
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : SemilatticeSup M
w : σ → M
⊢ weightedTotalDegree' w 0 = ⊥
simp only [weightedTotalDegree', support_zero, Finset.sup_empty]