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