no goals
ι : Type ?u.101051
ι' : Type ?u.101054
R : Type u_1
K : Type ?u.101060
A : Type u_2
A' : Type ?u.101066
A'' : Type ?u.101069
V : Type u
V' : Type ?u.101074
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
hx : AlgebraicIndependent R x
⊢ Injective ↑(algebraMap R A)
simpa [← MvPolynomial.algebraMap_eq, Function.comp] using
  (Injective.of_comp_iff (algebraicIndependent_iff_injective_aeval.1 hx) MvPolynomial.C).2
    (MvPolynomial.C_injective _ _)