ι : Type u_1
ι' : Type ?u.1278169
R : Type u_2
K : Type ?u.1278175
A : Type u_3
A' : Type ?u.1278181
A'' : Type ?u.1278184
V : Type u
V' : Type ?u.1278189
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
a : A
⊢ Injective (↑↑(Polynomial.aeval a) ∘ ↑(RingEquiv.toRingHom (mvPolynomialOptionEquivPolynomialAdjoin hx))) ↔
    Injective ↑(Polynomial.aeval a)
ι : Type u_1
ι' : Type ?u.1278169
R : Type u_2
K : Type ?u.1278175
A : Type u_3
A' : Type ?u.1278181
A'' : Type ?u.1278184
V : Type u
V' : Type ?u.1278189
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
a : A
⊢ (AlgebraicIndependent R fun o => Option.elim o a x) ↔ ¬_root_.IsAlgebraic { x_1 // x_1 ∈ adjoin R (range x) } a
rw [algebraicIndependent_iff_injective_aeval, isAlgebraic_iff_not_injective, Classical.not_not, ←
  AlgHom.coe_toRingHom, ← hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin,
  RingHom.coe_comp]
no goals
ι : Type u_1
ι' : Type ?u.1278169
R : Type u_2
K : Type ?u.1278175
A : Type u_3
A' : Type ?u.1278181
A'' : Type ?u.1278184
V : Type u
V' : Type ?u.1278189
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
a : A
⊢ Injective (↑↑(Polynomial.aeval a) ∘ ↑(RingEquiv.toRingHom (mvPolynomialOptionEquivPolynomialAdjoin hx))) ↔
    Injective ↑(Polynomial.aeval a)
exact Injective.of_comp_iff' (Polynomial.aeval a)
  (mvPolynomialOptionEquivPolynomialAdjoin hx).bijective