-- 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)
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
⊢ ∃ i, ⟨α, hα⟩ ∈ ↑(M i)

Tactic:
have ⟨β, hβ⟩ := h α

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
⊢ ∃ 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
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
let Ω := FS →ₐ[F] K'

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'
⊢ ↥(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
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
have splits s (hs : s ∈ S) : (minpoly F s).Splits (algebraMap F K') := by
  apply splits_of_splits_of_dvd _
    (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ minpoly.ne_zero <| (alg.isIntegral).1 _)
    ((splits_map_iff _ _).mp <| SplittingField.splits p) (Finset.dvd_prod_of_mem _ hs)

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)
⊢ ↥(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
s : E
hs : s ∈ S
⊢ Splits (algebraMap F K') (minpoly F s)

Tactic:
apply splits_of_splits_of_dvd _
  (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ minpoly.ne_zero <| (alg.isIntegral).1 _)
  ((splits_map_iff _ _).mp <| SplittingField.splits p) (Finset.dvd_prod_of_mem _ hs)

Result:
no goals

Proof state:
case inl
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
h✝ : Finite F
α : ↥FS
hα : F⟮α⟯ = ⊤
⊢ ∃ ω, ⊤ ≤ M ω

Tactic:
have ⟨ω, hω⟩ := Set.mem_iUnion.mp (this ▸ Set.mem_univ α)

Result:
case inl
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
h✝ : Finite F
α : ↥FS
hα : F⟮α⟯ = ⊤
ω : Ω
hω : α ∈ ↑(M ω)
⊢ ∃ ω, ⊤ ≤ M ω

Proof state:
case inl
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
h✝ : Finite F
⊢ ∃ ω, ⊤ ≤ M ω

Tactic:
have ⟨α, hα⟩ := exists_primitive_element_of_finite_bot F FS

Result:
case inl
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
h✝ : Finite F
α : ↥FS
hα : F⟮α⟯ = ⊤
⊢ ∃ ω, ⊤ ≤ M ω