no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.263576
r✝ : R
e✝ : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ vars (↑(monomial (Finsupp.single i e)) r) = {i}
rw [vars_monomial hr, Finsupp.support_single_ne_zero _ he]