-- Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
theorem IsTranscendenceBasis.isAlgebraic_field {F E : Type*} {x : ι → E}
    [Field F] [Field E] [Algebra F E] (hx : IsTranscendenceBasis F x) :
    Algebra.IsAlgebraic (IntermediateField.adjoin F (range x)) E

Proof state:
ι : Type u_1
F : Type u_7
E : Type u_8
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this : Algebra.IsAlgebraic (↥(adjoin F S)) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E

Tactic:
letI : Algebra (adjoin F S) (IntermediateField.adjoin F S) :=
  (Subalgebra.inclusion (IntermediateField.algebra_adjoin_le_adjoin F S)).toRingHom.toAlgebra

Result:
ι : Type u_1
F : Type u_7
E : Type u_8
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this✝ : Algebra.IsAlgebraic (↥(adjoin F S)) E
this : Algebra ↥(adjoin F S) ↥(IntermediateField.adjoin F S) := (Subalgebra.inclusion ⋯).toAlgebra
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E

Proof state:
ι : Type u_1
F : Type u_7
E : Type u_8
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this✝¹ : Algebra.IsAlgebraic (↥(adjoin F S)) E
this✝ : Algebra ↥(adjoin F S) ↥(IntermediateField.adjoin F S) := (Subalgebra.inclusion ⋯).toAlgebra
this : IsScalarTower (↥(adjoin F S)) (↥(IntermediateField.adjoin F S)) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E

Tactic:
exact Algebra.IsAlgebraic.extendScalars (R := adjoin F S) (Subalgebra.inclusion_injective _)

Result:
no goals

Proof state:
ι : Type u_1
F : Type u_7
E : Type u_8
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (range x))) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (range x))) E

Tactic:
set S := range x

Result:
ι : Type u_1
F : Type u_7
E : Type u_8
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this : Algebra.IsAlgebraic (↥(adjoin F S)) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E

Proof state:
ι : Type u_1
F : Type u_7
E : Type u_8
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (range x))) E

Tactic:
haveI := hx.isAlgebraic

Result:
ι : Type u_1
F : Type u_7
E : Type u_8
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (range x))) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (range x))) E

Proof state:
ι : Type u_1
F : Type u_7
E : Type u_8
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this✝ : Algebra.IsAlgebraic (↥(adjoin F S)) E
this : Algebra ↥(adjoin F S) ↥(IntermediateField.adjoin F S) := (Subalgebra.inclusion ⋯).toAlgebra
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E

Tactic:
haveI : IsScalarTower (adjoin F S) (IntermediateField.adjoin F S) E :=
  IsScalarTower.of_algebraMap_eq (congrFun rfl)

Result:
ι : Type u_1
F : Type u_7
E : Type u_8
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this✝¹ : Algebra.IsAlgebraic (↥(adjoin F S)) E
this✝ : Algebra ↥(adjoin F S) ↥(IntermediateField.adjoin F S) := (Subalgebra.inclusion ⋯).toAlgebra
this : IsScalarTower (↥(adjoin F S)) (↥(IntermediateField.adjoin F S)) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E