-- Mathlib/FieldTheory/Isaacs.lean
theorem nonempty_algHom_of_exist_roots (h : ∀ x : E, ∃ y : K, aeval y (minpoly F x) = 0) :
    Nonempty (E →ₐ[F] K)

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
let K₀ := (⊥ : IntermediateField K K').restrictScalars F

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
⊢ Nonempty (E →ₐ[F] K)

Tactic:
refine Lifts.nonempty_algHom_of_exist_lifts_finset fun S ↦ ⟨⟨adjoin F S, ?_⟩, subset_adjoin _ _⟩

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
let M (ω : Ω) := Subalgebra.toSubmodule (K₀.comap ω).toSubalgebra

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω => Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω => Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
x✝ : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : (aeval β) (minpoly F α) = 0
⊢ ∃ i, ⟨α, hα⟩ ∈ ↑(M i)

Tactic:
let ϕ : F⟮α⟯ →ₐ[F] K' := (IsScalarTower.toAlgHom _ _ _).comp ((AdjoinRoot.liftHom _ _ hβ).comp
  (adjoinRootEquivAdjoin F <| (alg.isIntegral).1 _).symm.toAlgHom)

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω => Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
x✝ : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : (aeval β) (minpoly F α) = 0
ϕ : ↥F⟮α⟯ →ₐ[F] K' :=
  (IsScalarTower.toAlgHom F K K').comp ((AdjoinRoot.liftHom (minpoly F α) β hβ).comp ↑(adjoinRootEquivAdjoin F ⋯).symm)
⊢ ∃ i, ⟨α, hα⟩ ∈ ↑(M i)

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω => Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
x✝ : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : (aeval β) (minpoly F α) = 0
ϕ : ↥F⟮α⟯ →ₐ[F] K' :=
  (IsScalarTower.toAlgHom F K K').comp ((AdjoinRoot.liftHom (minpoly F α) β hβ).comp ↑(adjoinRootEquivAdjoin F ⋯).symm)
ω : ↥(adjoin F (Membership.mem S.val)) →ₐ[F] K'
hω : ω.comp (inclusion ⋯) = ϕ
⊢ (IsScalarTower.toAlgHom F K K') β = (Algebra.ofId K K').toRingHom β

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω => Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
have : ⋃ ω : Ω, (M ω : Set FS) = Set.univ :=
  Set.eq_univ_of_forall fun ⟨α, hα⟩ ↦ Set.mem_iUnion.mpr <| by
    have ⟨β, hβ⟩ := h α
    let ϕ : F⟮α⟯ →ₐ[F] K' := (IsScalarTower.toAlgHom _ _ _).comp ((AdjoinRoot.liftHom _ _ hβ).comp
      (adjoinRootEquivAdjoin F <| (alg.isIntegral).1 _).symm.toAlgHom)
    have ⟨ω, hω⟩ := exists_algHom_adjoin_of_splits
      (fun s hs ↦ ⟨(alg.isIntegral).1 _, splits s hs⟩) ϕ (adjoin_simple_le_iff.mpr hα)
    refine ⟨ω, β, ((DFunLike.congr_fun hω <| AdjoinSimple.gen F α).trans ?_).symm⟩
    rw [AlgHom.comp_apply, AlgHom.comp_apply, AlgEquiv.coe_algHom,
      adjoinRootEquivAdjoin_symm_apply_gen, AdjoinRoot.liftHom_root]
    rfl

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this✝ : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω => Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
this : ⋃ ω, ↑(M ω) = Set.univ
⊢ ↥(adjoin F ↑S) →ₐ[F] K