no goals
ι : Type ?u.625472
ι' : Type ?u.625475
R : Type u_2
K : Type ?u.625481
A : Type u_1
A' : Type ?u.625487
A'' : Type ?u.625490
V : Type u
V' : Type ?u.625495
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
⊢ AlgebraicIndependent R Subtype.val ↔ ∀ (p : MvPolynomial A R), p ∈ supported R s → ↑(aeval _root_.id) p = 0 → p = 0
apply @algebraicIndependent_comp_subtype _ _ _ id