no goals
σ : Type u_1
τ : Type ?u.86982
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
i : ↑s
⊢ ↑(↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (X i)) = X ↑i
simp [supportedEquivMvPolynomial]