simp only [prod_empty, sum_empty]
case empty
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
⊢ (∅.prod id).support ⊆ ∅.sum support
case empty
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
⊢ support 1 ⊆ 0