-- 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:
case inr
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✝ : Infinite F
⊢ ∃ ω, ⊤ ≤ M ω

Tactic:
simp_rw [top_le_iff, Subspace.exists_eq_top_of_iUnion_eq_univ this]

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
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 ⋯) = ϕ
⊢ ϕ (AdjoinSimple.gen F α) = (Algebra.ofId K K').toRingHom β

Tactic:
rw [AlgHom.comp_apply, AlgHom.comp_apply, AlgEquiv.coe_algHom,
  adjoinRootEquivAdjoin_symm_apply_gen, AdjoinRoot.liftHom_root]

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)
ω : ↥(adjoin F (Membership.mem S.val)) →ₐ[F] K'
hω : ω.comp (inclusion ⋯) = ϕ
⊢ (IsScalarTower.toAlgHom F K K') β = (Algebra.ofId K K').toRingHom β

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

Tactic:
have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _

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

Tactic:
let p := (S.prod <| minpoly F).map (algebraMap 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))
⊢ ↥(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
this : ⋃ ω, ↑(M ω) = Set.univ
h✝ : Finite F
α : ↥FS
hα : F⟮α⟯ = ⊤
ω : Ω
hω : α ∈ ↑(M ω)
⊢ ⊤ ≤ comap ω K₀

Tactic:
rwa [← hα, adjoin_simple_le_iff]

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
this : ⋃ ω, ↑(M ω) = Set.univ
ω : ∃ ω, ⊤ ≤ M ω
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
exact ((botEquiv K K').toAlgHom.restrictScalars F).comp
  (ω.choose.codRestrict K₀.toSubalgebra fun x ↦ ω.choose_spec trivial)

Result:
no goals