-- Mathlib/RingTheory/Adjoin/Field.lean
theorem Polynomial.lift_of_splits {F K L : Type*} [Field F] [Field K] [Field L] [Algebra F K]
    [Algebra F L] (s : Finset K) : (∀ x ∈ s, IsIntegral F x ∧
      Splits (algebraMap F L) (minpoly F x)) → Nonempty (Algebra.adjoin F (s : Set K) →ₐ[F] L)

Proof state:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥Ks {a})) →ₐ[F] L)

Tactic:
have H5 : IsIntegral Ks a := H1.tower_top

Result:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥Ks {a})) →ₐ[F] L)

Proof state:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : ↥(Algebra.adjoin F ↑s) →ₐ[F] L
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)

Tactic:
rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]

Result:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : ↥(Algebra.adjoin F ↑s) →ₐ[F] L
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥(Algebra.adjoin F ↑s) {a})) →ₐ[F] L)

Proof state:
case refine_2.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)

Tactic:
obtain ⟨f⟩ := ih H3

Result:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : ↥(Algebra.adjoin F ↑s) →ₐ[F] L
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)

Proof state:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝ : FiniteDimensional F ↥Ks
this : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥Ks {a})) →ₐ[F] L)

Tactic:
letI := (f : Ks →+* L).toAlgebra

Result:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥Ks {a})) →ₐ[F] L)

Proof state:
case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
⊢ (aeval a) (map (algebraMap F ↥Ks) (minpoly F a)) = 0

Tactic:
rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]

Result:
no goals

Proof state:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥Ks {a})) →ₐ[F] L)

Tactic:
haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
  (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule

Result:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this : FiniteDimensional F ↥Ks
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥Ks {a})) →ₐ[F] L)