-- Mathlib/RingTheory/AlgebraicIndependent/AlgebraicClosure.lean
theorem extendScalars [alg : Algebra.IsAlgebraic R S] : AlgebraicIndependent S x

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i => x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝¹ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower (↥Rt) (↥St) A
this✝ : NoZeroDivisors ↥St
this : NoZeroDivisors ↥Rt
x✝ : ↥St
y : A
hy : y ∈ St
⊢ IsAlgebraic (↥Rt) y

Tactic:
have := Algebra.IsAlgebraic.nontrivial R S

Result:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i => x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝¹ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rt) (↥St) A
this✝¹ : NoZeroDivisors ↥St
this✝ : NoZeroDivisors ↥Rt
x✝ : ↥St
y : A
hy : y ∈ St
this : Nontrivial R
⊢ IsAlgebraic (↥Rt) y

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i => x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝³ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝³ : IsScalarTower (↥Rt) (↥St) A
this✝² : NoZeroDivisors ↥St
this✝¹ : NoZeroDivisors ↥Rt
x✝² : ↥St
y : A
hy : y ∈ St
this✝ : Nontrivial R
this : Nontrivial A
z : S
x✝¹ x✝ : R
eq : (algebraMap R ↥Rt) x✝¹ = (algebraMap R ↥Rt) x✝
⊢ x✝¹ = x✝

Tactic:
exact hx.algebraMap_injective congr($eq.1)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i => x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rt) (↥St) A
this✝¹ : NoZeroDivisors ↥St
this✝ : NoZeroDivisors ↥Rt
this : Algebra.IsAlgebraic ↥Rt ↥St
⊢ Transcendental (↥St) (x i)

Tactic:
exact (hx.transcendental_adjoin hi).extendScalars _

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i => x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower (↥Rt) (↥St) A
this✝ : NoZeroDivisors ↥St
this : NoZeroDivisors ↥Rt
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)

Tactic:
have : Algebra.IsAlgebraic Rt St := ⟨fun ⟨y, hy⟩ ↦ by
  rw [← isAlgebraic_algHom_iff (IsScalarTower.toAlgHom Rt St A) Subtype.val_injective]
  show IsAlgebraic Rt y
  have := Algebra.IsAlgebraic.nontrivial R S
  have := hx.algebraMap_injective.nontrivial
  exact adjoin_induction (fun _ h ↦ isAlgebraic_algebraMap (⟨_, subset_adjoin h⟩ : Rt))
    (fun z ↦ ((alg.1 z).algHom (IsScalarTower.toAlgHom R S A)).extendScalars fun _ _ eq ↦ by
      exact hx.algebraMap_injective congr($eq.1)) (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) hy⟩

Result:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i => x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rt) (↥St) A
this✝¹ : NoZeroDivisors ↥St
this✝ : NoZeroDivisors ↥Rt
this : Algebra.IsAlgebraic ↥Rt ↥St
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i => x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)

Tactic:
let St := adjoin S (x '' t)

Result:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i => x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)