awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
⊢ Function.Surjective.{u + 1, v + 1} (α := k) (β := K) (⇑(algebraMap k K) : (a : k) → K)

Tactic:
fun x => ⟨-(minpoly k x).coeff 0, ?_⟩

Premises used: minpoly, Polynomial.coeff, Exists.intro, OfNat.ofNat, Function.Surjective, Neg.neg
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
refine : ∀ (x : K), (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x
⊢ Function.Surjective.{u + 1, v + 1} (α := k) (β := K) (⇑(algebraMap k K) : (a : k) → K)

Tactic:
refine fun x => ⟨-(minpoly k x).coeff 0, ?_⟩
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
⊢ leadingCoeff (minpoly k x) = 1

Tactic:
have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (Algebra.IsSeparable.isIntegral k x)
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
⊢ IsSeparable k x

Tactic:
have hsep : IsSeparable k x := Algebra.IsSeparable.isSeparable k x
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : IsSeparable k x
⊢ degree (minpoly k x) = 1

Tactic:
have h : (minpoly k x).degree = 1 :=
    degree_eq_one_of_irreducible k (minpoly.irreducible (Algebra.IsSeparable.isIntegral k x)) hsep
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : IsSeparable k x
h : degree (minpoly k x) = 1
⊢ Eq.{v + 1} (α := K) ((aeval x : (a : k[X]) → K) (minpoly k x) : K) (0 : K)

Tactic:
have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : IsSeparable k x
h : degree (minpoly k x) = 1
this : Eq.{v + 1} (α := K) ((aeval x : (a : k[X]) → K) (minpoly k x) : K) (0 : K)
⊢ x = -(algebraMap k K : (a : k) → K) (coeff (minpoly k x) 0)

Tactic:
rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C,
    add_eq_zero_iff_eq_neg] at this

Premises used: Polynomial.C_1, Polynomial.eq_X_add_C_of_degree_eq_one, add_eq_zero_iff_eq_neg, Polynomial.aeval_C, Polynomial.aeval_add, one_mul, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : IsSeparable k x
h : degree (minpoly k x) = 1
this : x = -(algebraMap k K : (a : k) → K) (coeff (minpoly k x) 0)
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x

Tactic:
(map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm

Premises used: Algebra.algebraMap, Eq.rec, map_neg, minpoly, Polynomial.coeff, OfNat.ofNat, Eq.symm
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : IsSeparable k x
h : degree (minpoly k x) = 1
this : x = -(algebraMap k K : (a : k) → K) (coeff (minpoly k x) 0)
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x

Tactic:
exact (map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
L : IntermediateField k K
inst_4 : Algebra.IsSeparable.{u, v} k ↥L
x : K
hx : x ∈ L
obtain :
  ∀ (y : k) (hy : (algebraMap k ↥L : (a : k) → ↥L) y = Subtype.mk (p := fun (x : K) ↦ x ∈ L) x hx),
    Membership.mem (γ := IntermediateField k K) ⊥ x
⊢ Membership.mem (γ := IntermediateField k K) ⊥ x

Tactic:
obtain ⟨y, hy⟩ := IsSepClosed.algebraMap_surjective k L ⟨x, hx⟩

Premises used: Membership.mem, Subtype, Subtype.mk, IsSepClosed.algebraMap_surjective
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
L : IntermediateField k K
inst_4 : Algebra.IsSeparable.{u, v} k ↥L
x : K
hx : x ∈ L
y : k
hy : (algebraMap k ↥L : (a : k) → ↥L) y = Subtype.mk (p := fun (x : K) ↦ x ∈ L) x hx
⊢ Membership.mem (γ := IntermediateField k K) ⊥ x

Tactic:
⟨y, congr_arg (algebraMap L K) hy⟩

Premises used: Algebra.algebraMap, Set.Mem, setOf, Membership.mem, Subtype, congr_arg, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
L : IntermediateField k K
inst_4 : Algebra.IsSeparable.{u, v} k ↥L
x : K
hx : x ∈ L
y : k
hy : (algebraMap k ↥L : (a : k) → ↥L) y = Subtype.mk (p := fun (x : K) ↦ x ∈ L) x hx
⊢ Membership.mem (γ := IntermediateField k K) ⊥ x

Tactic:
exact ⟨y, congr_arg (algebraMap L K) hy⟩
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
⊢ IsSepClosed k

Tactic:
assumption
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsSepClosure k K
inst_4 : PerfectField K
⊢ IsAlgClosure k K

Tactic:
haveI : IsSepClosed K := IsSepClosure.sep_closed k
  ⟨inferInstance, IsSepClosure.separable.isAlgebraic⟩

Premises used: IsAlgClosure.mk, inferInstance, Algebra.IsSeparable.isAlgebraic
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsSepClosure k K
inst_4 : PerfectField k
⊢ IsAlgClosure k K

Tactic:
have halg : Algebra.IsAlgebraic k K := IsSepClosure.separable.isAlgebraic
  haveI := halg.perfectField; inferInstance

Premises used: inferInstance, Algebra.IsSeparable.isAlgebraic
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsAlgClosure k K
inst_4 : PerfectField k
⊢ IsSepClosure k K

Tactic:
⟨haveI := IsAlgClosure.isAlgClosed (R := k) (K := K); inferInstance,
    (IsAlgClosure.isAlgebraic (R := k) (K := K)).isSeparable_of_perfectField⟩

Premises used: inferInstance, IsSepClosure.mk, Algebra.IsAlgebraic.isSeparable_of_perfectField
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : Algebra k K
⊢ IsSepClosure k K ↔ IsSepClosed K ∧ Algebra.IsSeparable k K

Tactic:
⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

Premises used: And.right, And.left, IsSepClosure.mk, And.intro, Iff.intro, IsSepClosure.separable, IsSepClosure.sep_closed
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsSepClosure k K
⊢ Algebra.IsSeparable k K

Tactic:
IsSepClosure.separable

Premises used: IsSepClosure.separable
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
K : Type u
L : Type v
M : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : IsSepClosed M
E : Type u_1
inst_6 : Field E
inst_7 : Algebra K E
inst_8 : Algebra L E
inst_9 : IsScalarTower K L E
inst_10 : Algebra.IsSeparable L E
⊢ Function.Surjective (β := L →ₐ[K] M) fun (φ : E →ₐ[K] M) ↦ AlgHom.restrictDomain L φ

Tactic:
fun f ↦ IntermediateField.exists_algHom_of_splits' (E := E) f
    fun s ↦ ⟨Algebra.IsSeparable.isIntegral L s,
      IsSepClosed.splits_codomain _ <| Algebra.IsSeparable.isSeparable L s⟩

Premises used: Algebra.IsSeparable.isSeparable, IntermediateField.exists_algHom_of_splits', minpoly, IsSepClosed.splits_codomain, And.intro, Algebra.IsSeparable.isIntegral, Function.Surjective
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
⊢ Nonempty (E →ₐ[F] K)

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

Premises used: IntermediateField.subset_adjoin, SetLike.coe, IntermediateField.adjoin, Exists.intro, IntermediateField.Lifts.nonempty_algHom_of_exist_lifts_finset, IntermediateField.Lifts.mk
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
refine : (S : Finset E) → AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
⊢ Nonempty (E →ₐ[F] K)

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

Premises used: IntermediateField.subset_adjoin, SetLike.coe, IntermediateField.adjoin, Exists.intro, IntermediateField.Lifts.nonempty_algHom_of_exist_lifts_finset, IntermediateField.Lifts.mk
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
s : E
hs : s ∈ S
apply : Polynomial.map (algebraMap F K') (minpoly F s) ∣ Polynomial.map (algebraMap K p.SplittingField) p
⊢ (Polynomial.map (algebraMap F K') (minpoly F s)).Splits

Tactic:
apply (SplittingField.splits p).of_dvd (map_ne_zero (Finset.prod_ne_zero_iff.mpr
      fun _ _ ↦ Polynomial.map_ne_zero (minpoly.ne_zero <| alg.isIntegral.1 _))) ?_

Premises used: Iff.mpr, Algebra.IsIntegral.isIntegral, Finset.prod_ne_zero_iff, Polynomial.SplittingField.splits, Polynomial.Splits.of_dvd, Polynomial.map_ne_zero, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
s : E
hs : s ∈ S
rw : Polynomial.map (algebraMap F K) (minpoly F s) ∣ p
⊢ Polynomial.map (algebraMap F K') (minpoly F s) ∣ Polynomial.map (algebraMap K p.SplittingField) p

Tactic:
rw [IsScalarTower.algebraMap_eq F K K', ← Polynomial.map_map, map_dvd_map']

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map, Polynomial.map_dvd_map'
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
s : E
hs : s ∈ S
⊢ Polynomial.map (algebraMap F K) (minpoly F s) ∣ p

Tactic:
Finset.dvd_prod_of_mem _ hs

Premises used: Finset.dvd_prod_of_mem
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
s : E
hs : s ∈ S
⊢ Polynomial.map (algebraMap F K) (minpoly F s) ∣ p

Tactic:
exact Finset.dvd_prod_of_mem _ hs

Premises used: Finset.dvd_prod_of_mem
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
⊢ ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits

Tactic:
have splits s (hs : s ∈ S) : ((minpoly F s).map (algebraMap F K')).Splits := by
    apply (SplittingField.splits p).of_dvd (map_ne_zero (Finset.prod_ne_zero_iff.mpr
      fun _ _ ↦ Polynomial.map_ne_zero (minpoly.ne_zero <| alg.isIntegral.1 _))) ?_
    rw [IsScalarTower.algebraMap_eq F K K', ← Polynomial.map_map, map_dvd_map']
    exact Finset.dvd_prod_of_mem _ hs
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F (L' := K) ⊥
FS : IntermediateField F E := adjoin F (↑S : Set E)
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥FS) K'
⊢ FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))

Tactic:
have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F (L' := K) ⊥
FS : IntermediateField F E := adjoin F (↑S : Set E)
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥FS) K'
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
M : (ω : Ω) → Submodule F ↥FS :=
  fun (ω : Ω) ↦ (Subalgebra.toSubmodule : (a : Subalgebra F ↥FS) → Submodule F ↥FS) (comap ω K₀).toSubalgebra
x : ↥FS
α : E
hα : α ∈ FS
have :
  ∀ (β : K) (hβ : Eq.{u_3 + 1} (α := K) ((aeval β : (a : F[X]) → K) (minpoly F α) : K) (0 : K)),
    ∃ (i : Ω), Subtype.mk (p := fun (x : E) ↦ x ∈ FS) α hα ∈ (↑(M i) : Set ↥FS)
⊢ ∃ (i : Ω), Subtype.mk (p := fun (x : E) ↦ x ∈ FS) α hα ∈ (↑(M i) : Set ↥FS)

Tactic:
have ⟨β, hβ⟩ := h α
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F (L' := K) ⊥
FS : IntermediateField F E := adjoin F (↑S : Set E)
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥FS) K'
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
M : (ω : Ω) → Submodule F ↥FS :=
  fun (ω : Ω) ↦ (Subalgebra.toSubmodule : (a : Subalgebra F ↥FS) → Submodule F ↥FS) (comap ω K₀).toSubalgebra
x : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : Eq.{u_3 + 1} (α := K) ((aeval β : (a : F[X]) → K) (minpoly F α) : K) (0 : K)
ϕ : AlgHom.{u_1, u_2, u_3} F (↥F⟮α⟯) K' :=
  AlgHom.comp (IsScalarTower.toAlgHom F K K')
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp
      (↑(AlgEquiv.symm (adjoinRootEquivAdjoin F ⋯)) : ↥F⟮α⟯ →ₐ[F] AdjoinRoot (minpoly F α)))
have :
  ∀ (ω : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K') (hω : ω.comp (inclusion ⋯) = ϕ),
    ∃ (i : Ω), Subtype.mk (p := fun (x : E) ↦ x ∈ FS) α hα ∈ (↑(M i) : Set ↥FS)
⊢ ∃ (i : Ω), Subtype.mk (p := fun (x : E) ↦ x ∈ FS) α hα ∈ (↑(M i) : Set ↥FS)

Tactic:
have ⟨ω, hω⟩ := exists_algHom_adjoin_of_splits
        (fun s hs ↦ ⟨(alg.isIntegral).1 _, splits s hs⟩) ϕ (adjoin_simple_le_iff.mpr hα)
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F (L' := K) ⊥
FS : IntermediateField F E := adjoin F (↑S : Set E)
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥FS) K'
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
M : (ω : Ω) → Submodule F ↥FS :=
  fun (ω : Ω) ↦ (Subalgebra.toSubmodule : (a : Subalgebra F ↥FS) → Submodule F ↥FS) (comap ω K₀).toSubalgebra
x : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : Eq.{u_3 + 1} (α := K) ((aeval β : (a : F[X]) → K) (minpoly F α) : K) (0 : K)
ϕ : AlgHom.{u_1, u_2, u_3} F (↥F⟮α⟯) K' :=
  AlgHom.comp (IsScalarTower.toAlgHom F K K')
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp
      (↑(AlgEquiv.symm (adjoinRootEquivAdjoin F ⋯)) : ↥F⟮α⟯ →ₐ[F] AdjoinRoot (minpoly F α)))
ω : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K'
hω : ω.comp (inclusion ⋯) = ϕ
⊢ ∃ (i : Ω), Subtype.mk (p := fun (x : E) ↦ x ∈ FS) α hα ∈ (↑(M i) : Set ↥FS)

Tactic:
⟨ω, β, ((DFunLike.congr_fun hω <| AdjoinSimple.gen F α).trans ?_).symm⟩

Premises used: DFunLike.congr_fun, IntermediateField.AdjoinSimple.gen, Exists.intro, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F (L' := K) ⊥
FS : IntermediateField F E := adjoin F (↑S : Set E)
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥FS) K'
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
M : (ω : Ω) → Submodule F ↥FS :=
  fun (ω : Ω) ↦ (Subalgebra.toSubmodule : (a : Subalgebra F ↥FS) → Submodule F ↥FS) (comap ω K₀).toSubalgebra
x : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : Eq.{u_3 + 1} (α := K) ((aeval β : (a : F[X]) → K) (minpoly F α) : K) (0 : K)
ϕ : AlgHom.{u_1, u_2, u_3} F (↥F⟮α⟯) K' :=
  AlgHom.comp (IsScalarTower.toAlgHom F K K')
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp
      (↑(AlgEquiv.symm (adjoinRootEquivAdjoin F ⋯)) : ↥F⟮α⟯ →ₐ[F] AdjoinRoot (minpoly F α)))
ω : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K'
hω : ω.comp (inclusion ⋯) = ϕ
refine :
  Eq.{u_3 + 1} (α := K') ((ϕ : (a : ↥F⟮α⟯) → K') (AdjoinSimple.gen F α) : K')
    ((AlgHom.toRingHom (Algebra.ofId K K') : (a : K) → K') β : K')
⊢ ∃ (i : Ω), Subtype.mk (p := fun (x : E) ↦ x ∈ FS) α hα ∈ (↑(M i) : Set ↥FS)

Tactic:
refine ⟨ω, β, ((DFunLike.congr_fun hω <| AdjoinSimple.gen F α).trans ?_).symm⟩
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F (L' := K) ⊥
FS : IntermediateField F E := adjoin F (↑S : Set E)
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥FS) K'
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
M : (ω : Ω) → Submodule F ↥FS :=
  fun (ω : Ω) ↦ (Subalgebra.toSubmodule : (a : Subalgebra F ↥FS) → Submodule F ↥FS) (comap ω K₀).toSubalgebra
x : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : Eq.{u_3 + 1} (α := K) ((aeval β : (a : F[X]) → K) (minpoly F α) : K) (0 : K)
ϕ : AlgHom.{u_1, u_2, u_3} F (↥F⟮α⟯) K' :=
  AlgHom.comp (IsScalarTower.toAlgHom F K K')
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp
      (↑(AlgEquiv.symm (adjoinRootEquivAdjoin F ⋯)) : ↥F⟮α⟯ →ₐ[F] AdjoinRoot (minpoly F α)))
ω : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K'
hω : ω.comp (inclusion ⋯) = ϕ
rw :
  Eq (α := K') ((IsScalarTower.toAlgHom F K K' : (a : K) → K') β : K')
    ((AlgHom.toRingHom (Algebra.ofId K K') : (a : K) → K') β : K')
⊢ Eq.{u_3 + 1} (α := K') ((ϕ : (a : ↥F⟮α⟯) → K') (AdjoinSimple.gen F α) : K')
    ((AlgHom.toRingHom (Algebra.ofId K K') : (a : K) → K') β : K')

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

Premises used: IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen, AlgHom.comp_apply, AlgEquiv.coe_algHom, AdjoinRoot.liftAlgHom_root
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F (L' := K) ⊥
FS : IntermediateField F E := adjoin F (↑S : Set E)
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥FS) K'
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
M : (ω : Ω) → Submodule F ↥FS :=
  fun (ω : Ω) ↦ (Subalgebra.toSubmodule : (a : Subalgebra F ↥FS) → Submodule F ↥FS) (comap ω K₀).toSubalgebra
x : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : Eq.{u_3 + 1} (α := K) ((aeval β : (a : F[X]) → K) (minpoly F α) : K) (0 : K)
ϕ : AlgHom.{u_1, u_2, u_3} F (↥F⟮α⟯) K' :=
  AlgHom.comp (IsScalarTower.toAlgHom F K K')
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp
      (↑(AlgEquiv.symm (adjoinRootEquivAdjoin F ⋯)) : ↥F⟮α⟯ →ₐ[F] AdjoinRoot (minpoly F α)))
ω : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K'
hω : ω.comp (inclusion ⋯) = ϕ
⊢ Eq (α := K') ((IsScalarTower.toAlgHom F K K' : (a : K) → K') β : K')
    ((AlgHom.toRingHom (Algebra.ofId K K') : (a : K) → K') β : K')

Tactic:
rfl