no goals
σ : Type u_1
τ : Type ?u.126223
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ supported R Set.univ = ⊤
simp [Algebra.eq_top_iff, mem_supported]