[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : IsEmpty ι
⊢ AlgebraicIndependent R x ↔ Injective ↑(algebraMap R A)
[PROOFSTEP]
have : aeval x = (Algebra.ofId R A).comp (@isEmptyAlgEquiv R ι _ _).toAlgHom :=
  by
  ext i
  exact IsEmpty.elim' ‹IsEmpty ι› i
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : IsEmpty ι
⊢ aeval x = AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)
[PROOFSTEP]
ext i
[GOAL]
case hf
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : IsEmpty ι
i : ι
⊢ ↑(aeval x) (X i) = ↑(AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)) (X i)
[PROOFSTEP]
exact IsEmpty.elim' ‹IsEmpty ι› i
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : IsEmpty ι
this : aeval x = AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)
⊢ AlgebraicIndependent R x ↔ Injective ↑(algebraMap R A)
[PROOFSTEP]
rw [AlgebraicIndependent, this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R ι _ _).bijective]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : IsEmpty ι
this : aeval x = AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)
⊢ Injective ↑(AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)) ↔ Injective (↑(algebraMap R A) ∘ ↑(isEmptyAlgEquiv R ι))
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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)
[PROOFSTEP]
simpa [← MvPolynomial.algebraMap_eq, Function.comp] using
  (Injective.of_comp_iff (algebraicIndependent_iff_injective_aeval.1 hx) MvPolynomial.C).2
    (MvPolynomial.C_injective _ _)
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ LinearIndependent R x
[PROOFSTEP]
rw [linearIndependent_iff_injective_total]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 ↑(Finsupp.total ι A R x)
[PROOFSTEP]
have : Finsupp.total ι A R x = (MvPolynomial.aeval x).toLinearMap.comp (Finsupp.total ι _ R X) :=
  by
  ext
  simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ : ι
⊢ ↑(LinearMap.comp (Finsupp.total ι A R x) (Finsupp.lsingle a✝)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X))
          (Finsupp.lsingle a✝))
      1
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ Injective ↑(Finsupp.total ι A R x)
[PROOFSTEP]
rw [this]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ Injective ↑(LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X))
[PROOFSTEP]
refine' hx.comp _
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ Injective fun x => ↑(Finsupp.total ι (MvPolynomial ι R) R X) x
[PROOFSTEP]
rw [← linearIndependent_iff_injective_total]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ LinearIndependent R X
[PROOFSTEP]
exact linearIndependent_X _ _
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : ι' → ι
hf : Injective f
⊢ AlgebraicIndependent R (x ∘ f)
[PROOFSTEP]
intro p q
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : ι' → ι
hf : Injective f
p q : MvPolynomial ι' R
⊢ ↑(aeval (x ∘ f)) p = ↑(aeval (x ∘ f)) q → p = q
[PROOFSTEP]
simpa [aeval_rename, (rename_injective f hf).eq_iff] using @hx (rename f p) (rename f q)
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
simpa using hx.comp _ (rangeSplitting_injective x)
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
⊢ AlgebraicIndependent R (↑f ∘ x)
[PROOFSTEP]
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
⊢ aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
[PROOFSTEP]
ext
[GOAL]
case hf
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
i✝ : ι
⊢ ↑(aeval (↑f ∘ x)) (X i✝) = ↑(AlgHom.comp f (aeval x)) (X i✝)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ AlgebraicIndependent R (↑f ∘ x)
[PROOFSTEP]
have h : ∀ p : MvPolynomial ι R, aeval x p ∈ (@aeval R _ _ _ _ _ ((↑) : range x → A)).range :=
  by
  intro p
  rw [AlgHom.mem_range]
  refine' ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, _⟩
  simp [Function.comp, aeval_rename]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ ∀ (p : MvPolynomial ι R), ↑(aeval x) p ∈ AlgHom.range (aeval Subtype.val)
[PROOFSTEP]
intro p
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
p : MvPolynomial ι R
⊢ ↑(aeval x) p ∈ AlgHom.range (aeval Subtype.val)
[PROOFSTEP]
rw [AlgHom.mem_range]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
p : MvPolynomial ι R
⊢ ∃ x_1, ↑(aeval Subtype.val) x_1 = ↑(aeval x) p
[PROOFSTEP]
refine' ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, _⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
p : MvPolynomial ι R
⊢ ↑(aeval Subtype.val) (↑(rename (codRestrict x (range x) (_ : ∀ (i : ι), x i ∈ range fun x_1 => x x_1))) p) =
    ↑(aeval x) p
[PROOFSTEP]
simp [Function.comp, aeval_rename]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x) p ∈ AlgHom.range (aeval Subtype.val)
⊢ AlgebraicIndependent R (↑f ∘ x)
[PROOFSTEP]
intro x y hxy
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x✝))
this : aeval (↑f ∘ x✝) = AlgHom.comp f (aeval x✝)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x✝) p ∈ AlgHom.range (aeval Subtype.val)
x y : MvPolynomial ι R
hxy : ↑(aeval (↑f ∘ x✝)) x = ↑(aeval (↑f ∘ x✝)) y
⊢ x = y
[PROOFSTEP]
rw [this] at hxy 
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x✝))
this : aeval (↑f ∘ x✝) = AlgHom.comp f (aeval x✝)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x✝) p ∈ AlgHom.range (aeval Subtype.val)
x y : MvPolynomial ι R
hxy : ↑(AlgHom.comp f (aeval x✝)) x = ↑(AlgHom.comp f (aeval x✝)) y
⊢ x = y
[PROOFSTEP]
rw [adjoin_eq_range] at hf_inj 
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(AlgHom.range (aeval Subtype.val))
this : aeval (↑f ∘ x✝) = AlgHom.comp f (aeval x✝)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x✝) p ∈ AlgHom.range (aeval Subtype.val)
x y : MvPolynomial ι R
hxy : ↑(AlgHom.comp f (aeval x✝)) x = ↑(AlgHom.comp f (aeval x✝)) y
⊢ x = y
[PROOFSTEP]
exact hx (hf_inj (h x) (h y) hxy)
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
⊢ AlgebraicIndependent R x
[PROOFSTEP]
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
⊢ aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
[PROOFSTEP]
ext
[GOAL]
case hf
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
i✝ : ι
⊢ ↑(aeval (↑f ∘ x)) (X i✝) = ↑(AlgHom.comp f (aeval x)) (X i✝)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ AlgebraicIndependent R x
[PROOFSTEP]
rw [AlgebraicIndependent, this, AlgHom.coe_comp] at hfv 
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
f : A →ₐ[R] A'
hfv : Injective (↑f ∘ ↑(aeval x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ AlgebraicIndependent R x
[PROOFSTEP]
exact hfv.of_comp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K✝ : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
K : Type u_9
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ↑(algebraMap R K)
ai : AlgebraicIndependent K x
⊢ AlgebraicIndependent R x
[PROOFSTEP]
have :
  (aeval x : MvPolynomial ι K →ₐ[K] A).toRingHom.comp (MvPolynomial.map (algebraMap R K)) =
    (aeval x : MvPolynomial ι R →ₐ[R] A).toRingHom :=
  by ext <;> simp [algebraMap_eq_smul_one]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K✝ : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
K : Type u_9
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ↑(algebraMap R K)
ai : AlgebraicIndependent K x
⊢ RingHom.comp (↑(aeval x)) (MvPolynomial.map (algebraMap R K)) = ↑(aeval x)
[PROOFSTEP]
ext
[GOAL]
case hC.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
K✝ : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
K : Type u_9
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ↑(algebraMap R K)
ai : AlgebraicIndependent K x
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (↑(aeval x)) (MvPolynomial.map (algebraMap R K))) C) x✝ =
    ↑(RingHom.comp (↑(aeval x)) C) x✝
[PROOFSTEP]
simp [algebraMap_eq_smul_one]
[GOAL]
case hX
ι : Type u_1
ι' : Type u_2
R : Type u_3
K✝ : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
K : Type u_9
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ↑(algebraMap R K)
ai : AlgebraicIndependent K x
i✝ : ι
⊢ ↑(RingHom.comp (↑(aeval x)) (MvPolynomial.map (algebraMap R K))) (X i✝) = ↑↑(aeval x) (X i✝)
[PROOFSTEP]
simp [algebraMap_eq_smul_one]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K✝ : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
K : Type u_9
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ↑(algebraMap R K)
ai : AlgebraicIndependent K x
this : RingHom.comp (↑(aeval x)) (MvPolynomial.map (algebraMap R K)) = ↑(aeval x)
⊢ AlgebraicIndependent R x
[PROOFSTEP]
show Injective (aeval x).toRingHom
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K✝ : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
K : Type u_9
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ↑(algebraMap R K)
ai : AlgebraicIndependent K x
this : RingHom.comp (↑(aeval x)) (MvPolynomial.map (algebraMap R K)) = ↑(aeval x)
⊢ Injective ↑↑(aeval x)
[PROOFSTEP]
rw [← this, RingHom.coe_comp]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K✝ : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
K : Type u_9
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ↑(algebraMap R K)
ai : AlgebraicIndependent K x
this : RingHom.comp (↑(aeval x)) (MvPolynomial.map (algebraMap R K)) = ↑(aeval x)
⊢ Injective (↑↑(aeval x) ∘ ↑(MvPolynomial.map (algebraMap R K)))
[PROOFSTEP]
exact Injective.comp ai (MvPolynomial.map_injective _ hinj)
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
let f : t.map (Embedding.subtype s) → s := fun x =>
  ⟨x.1, by
    obtain ⟨x, h⟩ := x
    rw [Finset.mem_map] at h 
    obtain ⟨a, _, rfl⟩ := h
    simp only [Subtype.coe_prop, Embedding.coe_subtype]⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
x : { x // x ∈ Finset.map (Embedding.subtype s) t }
⊢ ↑x ∈ s
[PROOFSTEP]
obtain ⟨x, h⟩ := x
[GOAL]
case mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
x : A
h : x ∈ Finset.map (Embedding.subtype s) t
⊢ ↑{ val := x, property := h } ∈ s
[PROOFSTEP]
rw [Finset.mem_map] at h 
[GOAL]
case mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
x : A
h✝ : x ∈ Finset.map (Embedding.subtype s) t
h : ∃ a, a ∈ t ∧ ↑(Embedding.subtype s) a = x
⊢ ↑{ val := x, property := h✝ } ∈ s
[PROOFSTEP]
obtain ⟨a, _, rfl⟩ := h
[GOAL]
case mk.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
a : Subtype s
left✝ : a ∈ t
h : ↑(Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t
⊢ ↑{ val := ↑(Embedding.subtype s) a, property := h } ∈ s
[PROOFSTEP]
simp only [Subtype.coe_prop, Embedding.coe_subtype]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => { val := ↑x, property := (_ : ↑x ∈ s) }
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
convert AlgebraicIndependent.comp li f _
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => { val := ↑x, property := (_ : ↑x ∈ s) }
⊢ Injective f
[PROOFSTEP]
rintro ⟨x, hx⟩ ⟨y, hy⟩
[GOAL]
case mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => { val := ↑x, property := (_ : ↑x ∈ s) }
x : A
hx : x ∈ Finset.map (Embedding.subtype s) t
y : A
hy : y ∈ Finset.map (Embedding.subtype s) t
⊢ f { val := x, property := hx } = f { val := y, property := hy } →
    { val := x, property := hx } = { val := y, property := hy }
[PROOFSTEP]
rw [Finset.mem_map] at hx hy 
[GOAL]
case mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => { val := ↑x, property := (_ : ↑x ∈ s) }
x : A
hx✝ : x ∈ Finset.map (Embedding.subtype s) t
hx : ∃ a, a ∈ t ∧ ↑(Embedding.subtype s) a = x
y : A
hy✝ : y ∈ Finset.map (Embedding.subtype s) t
hy : ∃ a, a ∈ t ∧ ↑(Embedding.subtype s) a = y
⊢ f { val := x, property := hx✝ } = f { val := y, property := hy✝ } →
    { val := x, property := hx✝ } = { val := y, property := hy✝ }
[PROOFSTEP]
obtain ⟨a, _, rfl⟩ := hx
[GOAL]
case mk.mk.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => { val := ↑x, property := (_ : ↑x ∈ s) }
y : A
hy✝ : y ∈ Finset.map (Embedding.subtype s) t
hy : ∃ a, a ∈ t ∧ ↑(Embedding.subtype s) a = y
a : Subtype s
left✝ : a ∈ t
hx : ↑(Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t
⊢ f { val := ↑(Embedding.subtype s) a, property := hx } = f { val := y, property := hy✝ } →
    { val := ↑(Embedding.subtype s) a, property := hx } = { val := y, property := hy✝ }
[PROOFSTEP]
obtain ⟨b, _, rfl⟩ := hy
[GOAL]
case mk.mk.intro.intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => { val := ↑x, property := (_ : ↑x ∈ s) }
a : Subtype s
left✝¹ : a ∈ t
hx : ↑(Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t
b : Subtype s
left✝ : b ∈ t
hy : ↑(Embedding.subtype s) b ∈ Finset.map (Embedding.subtype s) t
⊢ f { val := ↑(Embedding.subtype s) a, property := hx } = f { val := ↑(Embedding.subtype s) b, property := hy } →
    { val := ↑(Embedding.subtype s) a, property := hx } = { val := ↑(Embedding.subtype s) b, property := hy }
[PROOFSTEP]
simp only [imp_self, Subtype.mk_eq_mk]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
⊢ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n
[PROOFSTEP]
intro s li
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ Cardinal.mk ↑s ≤ ↑n
[PROOFSTEP]
apply Cardinal.card_le_of
[GOAL]
case H
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), Finset.card s_1 ≤ n
[PROOFSTEP]
intro t
[GOAL]
case H
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card t ≤ n
[PROOFSTEP]
rw [← Finset.card_map (Embedding.subtype s)]
[GOAL]
case H
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card (Finset.map (Embedding.subtype s) t) ≤ n
[PROOFSTEP]
apply H
[GOAL]
case H.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R fun i => ↑i
[PROOFSTEP]
apply algebraicIndependent_finset_map_embedding_subtype _ li
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ AlgebraicIndependent R Subtype.val ↔ Injective ↑(algebraMap R A)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
t s : Set A
h : t ⊆ s
hx : AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
simpa [Function.comp] using hx.comp (inclusion h) (inclusion_injective h)
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
ι : Type u_9
f : ι → A
hf : AlgebraicIndependent R f
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
nontriviality R
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
ι : Type u_9
f : ι → A
hf : AlgebraicIndependent R f
✝ : Nontrivial R
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
rwa [algebraicIndependent_subtype_range hf.injective]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 ι
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ (p : MvPolynomial ι R), p ∈ supported R s → ↑(aeval x) p = 0 → p = 0
[PROOFSTEP]
have : (aeval (x ∘ (↑) : s → A) : _ →ₐ[R] _) = (aeval x).comp (rename (↑)) := by ext; simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 ι
⊢ aeval (x ∘ Subtype.val) = AlgHom.comp (aeval x) (rename Subtype.val)
[PROOFSTEP]
ext
[GOAL]
case hf
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 ι
i✝ : ↑s
⊢ ↑(aeval (x ∘ Subtype.val)) (X i✝) = ↑(AlgHom.comp (aeval x) (rename Subtype.val)) (X i✝)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 ι
this : aeval (x ∘ Subtype.val) = AlgHom.comp (aeval x) (rename Subtype.val)
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ (p : MvPolynomial ι R), p ∈ supported R s → ↑(aeval x) p = 0 → p = 0
[PROOFSTEP]
have : ∀ p : MvPolynomial s R, rename ((↑) : s → ι) p = 0 ↔ p = 0 :=
  (injective_iff_map_eq_zero' (rename ((↑) : s → ι) : MvPolynomial s R →ₐ[R] _).toRingHom).1
    (rename_injective _ Subtype.val_injective)
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 ι
this✝ : aeval (x ∘ Subtype.val) = AlgHom.comp (aeval x) (rename Subtype.val)
this : ∀ (p : MvPolynomial (↑s) R), ↑(rename Subtype.val) p = 0 ↔ p = 0
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ (p : MvPolynomial ι R), p ∈ supported R s → ↑(aeval x) p = 0 → p = 0
[PROOFSTEP]
simp [algebraicIndependent_iff, supported_eq_range_rename, *]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
[PROOFSTEP]
apply @algebraicIndependent_comp_subtype _ _ _ id
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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)
[PROOFSTEP]
simp
[GOAL]
ι✝ : Type u_1
ι'✝ : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
ι : Type u_9
ι' : Type u_10
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
⊢ AlgebraicIndependent R fun x => g ↑x
[PROOFSTEP]
nontriviality R
[GOAL]
ι✝ : Type u_1
ι'✝ : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
ι : Type u_9
ι' : Type u_10
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
⊢ AlgebraicIndependent R fun x => g ↑x
[PROOFSTEP]
have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
[GOAL]
ι✝ : Type u_1
ι'✝ : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
ι : Type u_9
ι' : Type u_10
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
this : InjOn f s
⊢ AlgebraicIndependent R fun x => g ↑x
[PROOFSTEP]
exact (algebraicIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
ι : Type u_9
s : Set ι
f : ι → A
hs : AlgebraicIndependent R fun x => f ↑x
⊢ AlgebraicIndependent R fun x => ↑x
[PROOFSTEP]
convert AlgebraicIndependent.image_of_comp s f id hs
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
η : Type u_9
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
refine' algebraicIndependent_of_finite (⋃ i, s i) fun t ht ft => _
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
η : Type u_9
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : Set.Finite t
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
η : Type u_9
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : Set.Finite t
I : Set η
fi : Set.Finite I
hI : t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
rcases hs.finset_le fi.toFinset with ⟨i, hi⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
η : Type u_9
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : Set.Finite t
I : Set η
fi : Set.Finite I
hI : t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
i : η
hi : ∀ (i_1 : η), i_1 ∈ Finite.toFinset fi → s i_1 ⊆ s i
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
letI : Nonempty s := Nonempty.to_subtype hsn
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
rw [sUnion_eq_iUnion]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ AlgebraicIndependent R Subtype.val
[PROOFSTEP]
exact algebraicIndependent_iUnion_of_directed hs.directed_val (by simpa using h)
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ ∀ (i : ↑s), AlgebraicIndependent R Subtype.val
[PROOFSTEP]
simpa using h
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
⊢ ∃ u,
    AlgebraicIndependent R Subtype.val ∧
      s ⊆ u ∧ u ⊆ t ∧ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → u ⊆ x → x ⊆ t → x = u
[PROOFSTEP]
rcases zorn_subset_nonempty {u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ s ⊆ u ∧ u ⊆ t}
    (fun c hc chainc hcn =>
      ⟨⋃₀ c,
        by
        refine' ⟨⟨algebraicIndependent_sUnion_of_directed hcn chainc.directedOn fun a ha => (hc ha).1, _, _⟩, _⟩
        · cases' hcn with x hx
          exact subset_sUnion_of_subset _ x (hc hx).2.1 hx
        · exact sUnion_subset fun x hx => (hc hx).2.2
        · intro s
          exact subset_sUnion_of_mem⟩)
    s ⟨hs, Set.Subset.refl s, hst⟩ with
  ⟨u, ⟨huai, _, hut⟩, hsu, hx⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t}
chainc : IsChain (fun x x_1 => x ⊆ x_1) c
hcn : Set.Nonempty c
⊢ ⋃₀ c ∈ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t} ∧ ∀ (s : Set A), s ∈ c → s ⊆ ⋃₀ c
[PROOFSTEP]
refine' ⟨⟨algebraicIndependent_sUnion_of_directed hcn chainc.directedOn fun a ha => (hc ha).1, _, _⟩, _⟩
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t}
chainc : IsChain (fun x x_1 => x ⊆ x_1) c
hcn : Set.Nonempty c
⊢ s ⊆ ⋃₀ c
[PROOFSTEP]
cases' hcn with x hx
[GOAL]
case refine'_1.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t}
chainc : IsChain (fun x x_1 => x ⊆ x_1) c
x : Set A
hx : x ∈ c
⊢ s ⊆ ⋃₀ c
[PROOFSTEP]
exact subset_sUnion_of_subset _ x (hc hx).2.1 hx
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t}
chainc : IsChain (fun x x_1 => x ⊆ x_1) c
hcn : Set.Nonempty c
⊢ ⋃₀ c ⊆ t
[PROOFSTEP]
exact sUnion_subset fun x hx => (hc hx).2.2
[GOAL]
case refine'_3
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t}
chainc : IsChain (fun x x_1 => x ⊆ x_1) c
hcn : Set.Nonempty c
⊢ ∀ (s : Set A), s ∈ c → s ⊆ ⋃₀ c
[PROOFSTEP]
intro s
[GOAL]
case refine'_3
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ t : Set A
hst : s✝ ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ s✝ ⊆ u ∧ u ⊆ t}
chainc : IsChain (fun x x_1 => x ⊆ x_1) c
hcn : Set.Nonempty c
s : Set A
⊢ s ∈ c → s ⊆ ⋃₀ c
[PROOFSTEP]
exact subset_sUnion_of_mem
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
u : Set A
huai : AlgebraicIndependent R Subtype.val
left✝ : s ⊆ u
hut : u ⊆ t
hsu : s ⊆ u
hx : ∀ (a : Set A), a ∈ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t} → u ⊆ a → a = u
⊢ ∃ u,
    AlgebraicIndependent R Subtype.val ∧
      s ⊆ u ∧ u ⊆ t ∧ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → u ⊆ x → x ⊆ t → x = u
[PROOFSTEP]
use u, huai, hsu, hut
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
u : Set A
huai : AlgebraicIndependent R Subtype.val
left✝ : s ⊆ u
hut : u ⊆ t
hsu : s ⊆ u
hx : ∀ (a : Set A), a ∈ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t} → u ⊆ a → a = u
⊢ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → u ⊆ x → x ⊆ t → x = u
[PROOFSTEP]
intro x hxai huv hxt
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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 t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
u : Set A
huai : AlgebraicIndependent R Subtype.val
left✝ : s ⊆ u
hut : u ⊆ t
hsu : s ⊆ u
hx : ∀ (a : Set A), a ∈ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t} → u ⊆ a → a = u
x : Set A
hxai : AlgebraicIndependent R Subtype.val
huv : u ⊆ x
hxt : x ⊆ t
⊢ x = u
[PROOFSTEP]
exact hx _ ⟨hxai, _root_.trans hsu huv, hxt⟩ huv
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ hx : AlgebraicIndependent R x
⊢ MvPolynomial ι R ≃ₐ[R] { x_1 // x_1 ∈ adjoin R (range x) }
[PROOFSTEP]
apply AlgEquiv.ofBijective (AlgHom.codRestrict (@aeval R A ι _ _ _ x) (Algebra.adjoin R (range x)) _)
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ hx : AlgebraicIndependent R x
⊢ Bijective ↑(AlgHom.codRestrict (aeval x) (adjoin R (range x)) ?m.935815)
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ hx : AlgebraicIndependent R x
⊢ ∀ (x_1 : MvPolynomial ι R), ↑(aeval x) x_1 ∈ adjoin R (range x)
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ hx : AlgebraicIndependent R x
⊢ ∀ (x_1 : MvPolynomial ι R), ↑(aeval x) x_1 ∈ adjoin R (range x)
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ hx : AlgebraicIndependent R x✝
x : MvPolynomial ι R
⊢ ↑(aeval x✝) x ∈ adjoin R (range x✝)
[PROOFSTEP]
rw [adjoin_range_eq_range_aeval]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ hx : AlgebraicIndependent R x✝
x : MvPolynomial ι R
⊢ ↑(aeval x✝) x ∈ AlgHom.range (aeval x✝)
[PROOFSTEP]
exact AlgHom.mem_range_self _ _
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ hx : AlgebraicIndependent R x
⊢ Bijective
    ↑(AlgHom.codRestrict (aeval x) (adjoin R (range x))
        (_ : ∀ (x_1 : MvPolynomial ι R), ↑(aeval x) x_1 ∈ adjoin R (range x)))
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ hx : AlgebraicIndependent R x
⊢ Injective
    ↑(AlgHom.codRestrict (aeval x) (adjoin R (range x))
        (_ : ∀ (x_1 : MvPolynomial ι R), ↑(aeval x) x_1 ∈ adjoin R (range x)))
[PROOFSTEP]
exact (AlgHom.injective_codRestrict _ _ _).2 hx
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝ hx : AlgebraicIndependent R x
⊢ Surjective
    ↑(AlgHom.codRestrict (aeval x) (adjoin R (range x))
        (_ : ∀ (x_1 : MvPolynomial ι R), ↑(aeval x) x_1 ∈ adjoin R (range x)))
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case right.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝¹ hx✝ : AlgebraicIndependent R x✝
x : A
hx : x ∈ adjoin R (range x✝)
⊢ ∃ a,
    ↑(AlgHom.codRestrict (aeval x✝) (adjoin R (range x✝))
            (_ : ∀ (x : MvPolynomial ι R), ↑(aeval x✝) x ∈ adjoin R (range x✝)))
        a =
      { val := x, property := hx }
[PROOFSTEP]
rw [adjoin_range_eq_range_aeval] at hx 
[GOAL]
case right.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝² hx✝¹ : AlgebraicIndependent R x✝
x : A
hx✝ : x ∈ adjoin R (range x✝)
hx : x ∈ AlgHom.range (aeval x✝)
⊢ ∃ a,
    ↑(AlgHom.codRestrict (aeval x✝) (adjoin R (range x✝))
            (_ : ∀ (x : MvPolynomial ι R), ↑(aeval x✝) x ∈ adjoin R (range x✝)))
        a =
      { val := x, property := hx✝ }
[PROOFSTEP]
rcases hx with ⟨y, rfl⟩
[GOAL]
case right.mk.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝¹ hx✝ : AlgebraicIndependent R x
y : MvPolynomial ι R
hx : ↑↑(aeval x) y ∈ adjoin R (range x)
⊢ ∃ a,
    ↑(AlgHom.codRestrict (aeval x) (adjoin R (range x))
            (_ : ∀ (x_1 : MvPolynomial ι R), ↑(aeval x) x_1 ∈ adjoin R (range x)))
        a =
      { val := ↑↑(aeval x) y, property := hx }
[PROOFSTEP]
use y
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝¹ hx✝ : AlgebraicIndependent R x
y : MvPolynomial ι R
hx : ↑↑(aeval x) y ∈ adjoin R (range x)
⊢ ↑(AlgHom.codRestrict (aeval x) (adjoin R (range x))
          (_ : ∀ (x_1 : MvPolynomial ι R), ↑(aeval x) x_1 ∈ adjoin R (range x)))
      y =
    { val := ↑↑(aeval x) y, property := hx }
[PROOFSTEP]
ext
[GOAL]
case h.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝¹ hx✝ : AlgebraicIndependent R x
y : MvPolynomial ι R
hx : ↑↑(aeval x) y ∈ adjoin R (range x)
⊢ ↑(↑(AlgHom.codRestrict (aeval x) (adjoin R (range x))
            (_ : ∀ (x_1 : MvPolynomial ι R), ↑(aeval x) x_1 ∈ adjoin R (range x)))
        y) =
    ↑{ val := ↑↑(aeval x) y, property := hx }
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
r : R
⊢ ↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (↑C r) =
    ↑Polynomial.C (↑(algebraMap R { x_1 // x_1 ∈ adjoin R (range x) }) r)
[PROOFSTEP]
rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_C,
  IsScalarTower.algebraMap_apply R (MvPolynomial ι R), ← Polynomial.C_eq_algebraMap, Polynomial.map_C, RingHom.coe_coe,
  AlgEquiv.commutes]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ ↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X none) = Polynomial.X
[PROOFSTEP]
rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim, Polynomial.map_X]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
i : ι
⊢ ↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X (some i)) = ↑Polynomial.C (↑(aevalEquiv hx) (X i))
[PROOFSTEP]
rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim, Polynomial.map_C,
  RingHom.coe_coe]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ RingHom.comp (↑(Polynomial.aeval a)) (RingEquiv.toRingHom (mvPolynomialOptionEquivPolynomialAdjoin hx)) =
    ↑(aeval fun o => Option.elim o a x)
[PROOFSTEP]
refine' MvPolynomial.ringHom_ext _ _
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ ∀ (r : R),
    ↑(RingHom.comp (↑(Polynomial.aeval a)) (RingEquiv.toRingHom (mvPolynomialOptionEquivPolynomialAdjoin hx))) (↑C r) =
      ↑↑(aeval fun o => Option.elim o a x) (↑C r)
[PROOFSTEP]
simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom, AlgHom.coe_toRingHom,
  AlgHom.coe_toRingHom]
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ ∀ (i : Option ι),
    ↑(RingHom.comp (↑(Polynomial.aeval a)) (RingEquiv.toRingHom (mvPolynomialOptionEquivPolynomialAdjoin hx))) (X i) =
      ↑↑(aeval fun o => Option.elim o a x) (X i)
[PROOFSTEP]
simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom, AlgHom.coe_toRingHom,
  AlgHom.coe_toRingHom]
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ ∀ (r : R),
    ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (↑C r)) =
      ↑(aeval fun o => Option.elim o a x) (↑C r)
[PROOFSTEP]
intro r
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
r : R
⊢ ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (↑C r)) =
    ↑(aeval fun o => Option.elim o a x) (↑C r)
[PROOFSTEP]
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
  IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ ∀ (i : Option ι),
    ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X i)) =
      ↑(aeval fun o => Option.elim o a x) (X i)
[PROOFSTEP]
rintro (⟨⟩ | ⟨i⟩)
[GOAL]
case refine'_2.none
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
⊢ ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X none)) =
    ↑(aeval fun o => Option.elim o a x) (X none)
[PROOFSTEP]
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X, Option.elim]
[GOAL]
case refine'_2.some
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
i : ι
⊢ ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X (some i))) =
    ↑(aeval fun o => Option.elim o a x) (X (some i))
[PROOFSTEP]
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C, hx.algebraMap_aevalEquiv, aeval_X, aeval_X,
  Option.elim]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
[PROOFSTEP]
rw [algebraicIndependent_iff_injective_aeval, isAlgebraic_iff_not_injective, Classical.not_not, ← AlgHom.coe_toRingHom,
  ← hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, RingHom.coe_comp]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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)
[PROOFSTEP]
exact Injective.of_comp_iff' (Polynomial.aeval a) (mvPolynomialOptionEquivPolynomialAdjoin hx).bijective
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
h : Injective ↑(algebraMap R A)
⊢ ∃ s, IsTranscendenceBasis R Subtype.val
[PROOFSTEP]
cases'
  exists_maximal_algebraicIndependent (∅ : Set A) Set.univ (Set.subset_univ _)
    ((algebraicIndependent_empty_iff R A).2 h) with
  s hs
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
h : Injective ↑(algebraMap R A)
s : Set A
hs :
  AlgebraicIndependent R Subtype.val ∧
    ∅ ⊆ s ∧ s ⊆ univ ∧ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → s ⊆ x → x ⊆ univ → x = s
⊢ ∃ s, IsTranscendenceBasis R Subtype.val
[PROOFSTEP]
use s, hs.1
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
h : Injective ↑(algebraMap R A)
s : Set A
hs :
  AlgebraicIndependent R Subtype.val ∧
    ∅ ⊆ s ∧ s ⊆ univ ∧ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → s ⊆ x → x ⊆ univ → x = s
⊢ ∀ (s_1 : Set A), AlgebraicIndependent R Subtype.val → range Subtype.val ≤ s_1 → range Subtype.val = s_1
[PROOFSTEP]
intro t ht hr
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
h : Injective ↑(algebraMap R A)
s : Set A
hs :
  AlgebraicIndependent R Subtype.val ∧
    ∅ ⊆ s ∧ s ⊆ univ ∧ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → s ⊆ x → x ⊆ univ → x = s
t : Set A
ht : AlgebraicIndependent R Subtype.val
hr : range Subtype.val ≤ t
⊢ range Subtype.val = t
[PROOFSTEP]
simp only [Subtype.range_coe_subtype, setOf_mem_eq] at *
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
h : Injective ↑(algebraMap R A)
s : Set A
hs :
  AlgebraicIndependent R Subtype.val ∧
    ∅ ⊆ s ∧ s ⊆ univ ∧ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → s ⊆ x → x ⊆ univ → x = s
t : Set A
ht : AlgebraicIndependent R Subtype.val
hr : s ≤ t
⊢ s = t
[PROOFSTEP]
exact Eq.symm (hs.2.2.2 t ht hr (Set.subset_univ _))
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
⊢ IsTranscendenceBasis R x ↔
    ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
[PROOFSTEP]
fconstructor
[GOAL]
case mp
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
⊢ IsTranscendenceBasis R x →
    ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
[PROOFSTEP]
rintro p κ w i' j rfl
[GOAL]
case mp
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
κ : Type v
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p : IsTranscendenceBasis R (w ∘ j)
⊢ Surjective j
[PROOFSTEP]
have p := p.2 (range w) i'.coe_range (range_comp_subset_range _ _)
[GOAL]
case mp
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
κ : Type v
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : range (w ∘ j) = range w
⊢ Surjective j
[PROOFSTEP]
rw [range_comp, ← @image_univ _ _ w] at p 
[GOAL]
case mp
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
κ : Type v
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j
[PROOFSTEP]
exact range_iff_surjective.mp (image_injective.mpr i'.injective p)
[GOAL]
case mpr
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
⊢ (∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j) →
    IsTranscendenceBasis R x
[PROOFSTEP]
intro p
[GOAL]
case mpr
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ IsTranscendenceBasis R x
[PROOFSTEP]
use i
[GOAL]
case right
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → range x ≤ s → range x = s
[PROOFSTEP]
intro w i' h
[GOAL]
case right
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
⊢ range x = w
[PROOFSTEP]
specialize p w ((↑) : w → A) i' (fun i => ⟨x i, range_subset_iff.mp h i⟩) (by ext; simp)
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
⊢ (Subtype.val ∘ fun i => { val := x i, property := (_ : x i ∈ w) }) = x
[PROOFSTEP]
ext
[GOAL]
case h
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
x✝ : ι
⊢ (Subtype.val ∘ fun i => { val := x i, property := (_ : x i ∈ w) }) x✝ = x x✝
[PROOFSTEP]
simp
[GOAL]
case right
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => { val := x i, property := (_ : x i ∈ w) }
⊢ range x = w
[PROOFSTEP]
have q := congr_arg (fun s => ((↑) : w → A) '' s) p.range_eq
[GOAL]
case right
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => { val := x i, property := (_ : x i ∈ w) }
q :
  (fun s => Subtype.val '' s) (range fun i => { val := x i, property := (_ : x i ∈ w) }) =
    (fun s => Subtype.val '' s) univ
⊢ range x = w
[PROOFSTEP]
dsimp at q 
[GOAL]
case right
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => { val := x i, property := (_ : x i ∈ w) }
q : (Subtype.val '' range fun i => { val := x i, property := (_ : x i ∈ w) }) = Subtype.val '' univ
⊢ range x = w
[PROOFSTEP]
rw [← image_univ, image_image] at q 
[GOAL]
case right
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
K : Type u_4
A✝ : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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✝
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => { val := x i, property := (_ : x i ∈ w) }
q : (fun x_1 => ↑{ val := x x_1, property := (_ : x x_1 ∈ w) }) '' univ = Subtype.val '' univ
⊢ range x = w
[PROOFSTEP]
simpa using q
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ Algebra.IsAlgebraic { x_1 // x_1 ∈ adjoin R (range x) } A
[PROOFSTEP]
intro a
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ _root_.IsAlgebraic { x_1 // x_1 ∈ adjoin R (range x) } a
[PROOFSTEP]
rw [← not_iff_comm.1 (hx.1.option_iff _).symm]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ ¬AlgebraicIndependent R fun o => Option.elim o a x
[PROOFSTEP]
intro ai
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
⊢ False
[PROOFSTEP]
have h₁ : range x ⊆ range fun o : Option ι => o.elim a x :=
  by
  rintro x ⟨y, rfl⟩
  exact ⟨some y, rfl⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
⊢ range x ⊆ range fun o => Option.elim o a x
[PROOFSTEP]
rintro x ⟨y, rfl⟩
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
y : ι
⊢ x y ∈ range fun o => Option.elim o a x
[PROOFSTEP]
exact ⟨some y, rfl⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
⊢ False
[PROOFSTEP]
have h₂ : range x ≠ range fun o : Option ι => o.elim a x :=
  by
  intro h
  have : a ∈ range x := by
    rw [h]
    exact ⟨none, rfl⟩
  rcases this with ⟨b, rfl⟩
  have : some b = none := ai.injective rfl
  simpa
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
⊢ range x ≠ range fun o => Option.elim o a x
[PROOFSTEP]
intro h
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
⊢ False
[PROOFSTEP]
have : a ∈ range x := by
  rw [h]
  exact ⟨none, rfl⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
⊢ a ∈ range x
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
⊢ a ∈ range fun o => Option.elim o a x
[PROOFSTEP]
exact ⟨none, rfl⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
this : a ∈ range x
⊢ False
[PROOFSTEP]
rcases this with ⟨b, rfl⟩
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => Option.elim o (x b) x
h₁ : range x ⊆ range fun o => Option.elim o (x b) x
h : range x = range fun o => Option.elim o (x b) x
⊢ False
[PROOFSTEP]
have : some b = none := ai.injective rfl
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => Option.elim o (x b) x
h₁ : range x ⊆ range fun o => Option.elim o (x b) x
h : range x = range fun o => Option.elim o (x b) x
this : some b = none
⊢ False
[PROOFSTEP]
simpa
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h₂ : range x ≠ range fun o => Option.elim o a x
⊢ False
[PROOFSTEP]
exact h₂ (hx.2 (Set.range fun o : Option ι => o.elim a x) ((algebraicIndependent_subtype_range ai.injective).2 ai) h₁)
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ AlgebraicIndependent K x
[PROOFSTEP]
rw [algebraicIndependent_empty_type_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
A'' : Type u_7
V : Type u
V' : Type u_8
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
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ Injective ↑(algebraMap K A)
[PROOFSTEP]
exact RingHom.injective _
