no goals
σ : Type u_1
τ : Type ?u.128582
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
i : σ
⊢ X i ∈ supported R s ↔ i ∈ s
simp [mem_supported]