no goals
ι : Type ?u.745808
ι' : Type ?u.745811
R : Type u_2
K : Type ?u.745817
A : Type u_1
A' : Type ?u.745823
A'' : Type ?u.745826
V : Type u
V' : Type ?u.745831
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
s : Set A
H : ∀ (t : Set A), t ⊆ s → Set.Finite t → AlgebraicIndependent R Subtype.val
p : MvPolynomial A R
hp : p ∈ supported R s
⊢ p ∈ supported R ↑(vars p)
simp