-- 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:
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
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)

Tactic:
refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_

Result:
case refine_1
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
x✝ : ∀ x ∈ ∅, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty (↥(Algebra.adjoin F ↑∅) →ₐ[F] L)

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
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ 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
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)

Tactic:
set Ks := Algebra.adjoin F (s : Set K)

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
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥Ks {a})) →ₐ[F] L)

Proof state:
case refine_1
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
⊢ Splits ((algebraMap (↥Ks) L).comp (algebraMap F ↥Ks)) (minpoly F a)

Tactic:
rw [← IsScalarTower.algebraMap_eq]

Result:
case refine_1
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
⊢ Splits (algebraMap F L) (minpoly F a)

Proof state:
case refine_1
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
x✝ : ∀ x ∈ ∅, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty (↥⊥ →ₐ[F] L)

Tactic:
exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩

Result:
no goals

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
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)

Tactic:
rw [forall_mem_insert] at H

Result:
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
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H :
  (IsIntegral F a ∧ Splits (algebraMap F L) (minpoly F a)) ∧
    ∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[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
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H :
  (IsIntegral F a ∧ Splits (algebraMap F L) (minpoly F a)) ∧
    ∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)

Tactic:
rcases H with ⟨⟨H1, H2⟩, H3⟩

Result:
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)