-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem algebraicIndependent_polynomial_aeval_X
    (f : ι → Polynomial R) (hf : ∀ i, Transcendental R (f i)) :
    AlgebraicIndependent R fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i)

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
⊢ AlgebraicIndependent R fun i => (Polynomial.aeval (X i)) (f i)

Tactic:
set x := fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i)

Result:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
⊢ AlgebraicIndependent R x

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
hle : adjoin R (x '' t) ≤ supported R t
⊢ Transcendental (↥(adjoin R (x '' t))) (x i)

Tactic:
exact (transcendental_supported_polynomial_aeval_X R hi (hf i)).of_tower_top_of_subalgebra_le hle

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ x a✝ ∈ ↑(supported R t)

Tactic:
refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)

Result:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ {X a✝} ⊆ X '' t

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
⊢ Transcendental (↥(adjoin R (x '' t))) (x i)

Tactic:
have hle : adjoin R (x '' t) ≤ supported R t := by
  rw [Algebra.adjoin_le_iff, Set.image_subset_iff]
  intro _ h
  rw [Set.mem_preimage]
  refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)
  simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]

Result:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
hle : adjoin R (x '' t) ≤ supported R t
⊢ Transcendental (↥(adjoin R (x '' t))) (x i)

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ {X a✝} ⊆ X '' t

Tactic:
simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ a✝ ∈ x ⁻¹' ↑(supported R t)

Tactic:
rw [Set.mem_preimage]

Result:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ x a✝ ∈ ↑(supported R t)

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
⊢ t ⊆ x ⁻¹' ↑(supported R t)

Tactic:
intro _ h

Result:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ a✝ ∈ x ⁻¹' ↑(supported R t)

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
⊢ adjoin R (x '' t) ≤ supported R t

Tactic:
rw [Algebra.adjoin_le_iff, Set.image_subset_iff]

Result:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
⊢ t ⊆ x ⁻¹' ↑(supported R t)

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
⊢ AlgebraicIndependent R x

Tactic:
refine algebraicIndependent_of_finite_type' (C_injective _ _) fun t _ _ i hi ↦ ?_

Result:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i => (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i => x ↑i
i : ι
hi : i ∉ t
⊢ Transcendental (↥(adjoin R (x '' t))) (x i)