awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq.{u_2 + 1} (α := Set ↥FS) (⋃ (ω : Ω), (↑(M ω) : Set ↥FS)) Set.univ

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.liftAlgHom _ _ _ 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.liftAlgHom_root]
      rfl
-- 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_1 : 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
this : Eq.{u_2 + 1} (α := Set ↥FS) (⋃ (ω : Ω), (↑(M ω) : Set ↥FS)) Set.univ
inl : Finite F → ∃ (ω : Ω), ⊤ ≤ M ω
inr : Infinite F → ∃ (ω : Ω), ⊤ ≤ M ω
⊢ ∃ (ω : Ω), ⊤ ≤ M ω

Tactic:
cases finite_or_infinite F

Premises used: finite_or_infinite
-- 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_1 : 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
this : Eq.{u_2 + 1} (α := Set ↥FS) (⋃ (ω : Ω), (↑(M ω) : Set ↥FS)) Set.univ
h_1 : Finite F
inl : ∀ (α : ↥FS) (hα : Eq (α := IntermediateField F ↥FS) F⟮α⟯ ⊤), ∃ (ω : Ω), ⊤ ≤ M ω
⊢ ∃ (ω : Ω), ⊤ ≤ M ω

Tactic:
have ⟨α, hα⟩ := exists_primitive_element_of_finite_bot F FS
-- 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_1 : 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
this : Eq.{u_2 + 1} (α := Set ↥FS) (⋃ (ω : Ω), (↑(M ω) : Set ↥FS)) Set.univ
h_1 : Finite F
α : ↥FS
hα : Eq (α := IntermediateField F ↥FS) F⟮α⟯ ⊤
inl : ∀ (ω : Ω) (hω : α ∈ (↑(M ω) : Set ↥FS)), ∃ (ω : Ω), ⊤ ≤ M ω
⊢ ∃ (ω : Ω), ⊤ ≤ M ω

Tactic:
have ⟨ω, hω⟩ := Set.mem_iUnion.mp (this ▸ Set.mem_univ α)
-- 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_1 : 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
this : Eq.{u_2 + 1} (α := Set ↥FS) (⋃ (ω : Ω), (↑(M ω) : Set ↥FS)) Set.univ
h_1 : Finite F
α : ↥FS
hα : Eq (α := IntermediateField F ↥FS) F⟮α⟯ ⊤
ω : Ω
hω : α ∈ (↑(M ω) : Set ↥FS)
rwa : F⟮α⟯ ≤ comap ω K₀
rwa₁ rwa₂ rwa₃ rwa₄ : α ∈ comap ω K₀
⊢ ⊤ ≤ comap ω K₀

Tactic:
rwa [← hα, adjoin_simple_le_iff]

Premises used: IntermediateField.adjoin_simple_le_iff
-- 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_1 : 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
this : Eq.{u_2 + 1} (α := Set ↥FS) (⋃ (ω : Ω), (↑(M ω) : Set ↥FS)) Set.univ
h_1 : Finite F
α : ↥FS
hα : Eq (α := IntermediateField F ↥FS) F⟮α⟯ ⊤
ω : Ω
hω : α ∈ (↑(M ω) : Set ↥FS)
⊢ ∃ (ω : Ω), ⊤ ≤ M ω

Tactic:
exact ⟨ω, show ⊤ ≤ K₀.comap ω by rwa [← hα, adjoin_simple_le_iff]⟩
-- 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_1 : 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
this : Eq.{u_2 + 1} (α := Set ↥FS) (⋃ (ω : Ω), (↑(M ω) : Set ↥FS)) Set.univ
h_1 : Infinite F
inr : ∃ (ω : Ω), M ω = ⊤
⊢ ∃ (ω : Ω), ⊤ ≤ M ω

Tactic:
simp_rw [top_le_iff, Subspace.exists_eq_top_of_iUnion_eq_univ this]

Premises used: Subspace.exists_eq_top_of_iUnion_eq_univ, top_le_iff
-- 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_1 : 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
this : Eq.{u_2 + 1} (α := Set ↥FS) (⋃ (ω : Ω), (↑(M ω) : Set ↥FS)) Set.univ
⊢ ∃ (ω : Ω), ⊤ ≤ M ω

Tactic:
have ω : ∃ ω : Ω, ⊤ ≤ M ω := by
    cases finite_or_infinite F
    · have ⟨α, hα⟩ := exists_primitive_element_of_finite_bot F FS
      have ⟨ω, hω⟩ := Set.mem_iUnion.mp (this ▸ Set.mem_univ α)
      exact ⟨ω, show ⊤ ≤ K₀.comap ω by rwa [← hα, adjoin_simple_le_iff]⟩
    · simp_rw [top_le_iff, Subspace.exists_eq_top_of_iUnion_eq_univ this]
-- 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_1 : 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
this : Eq.{u_2 + 1} (α := Set ↥FS) (⋃ (ω : Ω), (↑(M ω) : Set ↥FS)) Set.univ
ω : ∃ (ω : Ω), ⊤ ≤ M ω
⊢ AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K

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

Premises used: Exists.choose_spec, trivial, AlgEquiv.toAlgHom, AlgHom.restrictScalars, Exists.choose, AlgHom.codRestrict, AlgHom.comp, IntermediateField.botEquiv, IntermediateField.toSubalgebra
-- 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 (α := F[X]) (minpoly F x) (minpoly F y)
x : E
y : K
hy : Eq (α := F[X]) (minpoly F x) (minpoly F y)
rw : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F y) : K) (0 : K)
rw₁ rw₂ : Eq.{u_3 + 1} (α := K) 0 0
⊢ Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)

Tactic:
rw [hy, minpoly.aeval]

Premises used: minpoly.aeval
-- 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 :
  Subset (α := Set F[X]) (Set.range.{u_1, u_2 + 1} (ι := E) (minpoly F)) (Set.range.{u_1, u_3 + 1} (ι := K) (minpoly F))
⊢ Nonempty (E →ₐ[F] K)

Tactic:
nonempty_algHom_of_minpoly_eq fun x ↦ have ⟨y, hy⟩ := h ⟨x, rfl⟩; ⟨y, hy.symm⟩

Premises used: Exists, minpoly, Exists.intro, Field.nonempty_algHom_of_minpoly_eq, Eq.symm, Eq, rfl, _private.0.Field.nonempty_algHom_of_range_minpoly_subset.match_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 : Eq (α := Set F[X]) (Set.range.{u_1, u_2 + 1} (ι := E) (minpoly F)) (Set.range.{u_1, u_3 + 1} (ι := K) (minpoly F))
σ : E →ₐ[F] K
y : K
by_contra : ∀ (hy : ¬IsIntegral F y), False
⊢ IsIntegral F y

Tactic:
by_contra hy
-- 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 : Eq (α := Set F[X]) (Set.range.{u_1, u_2 + 1} (ι := E) (minpoly F)) (Set.range.{u_1, u_3 + 1} (ι := K) (minpoly F))
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
have : ∀ (x : E) (hx : Eq (α := F[X]) (minpoly F x) (minpoly F y)), False
⊢ False

Tactic:
have ⟨x, hx⟩ := h.ge ⟨y, rfl⟩
-- 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 : Eq (α := Set F[X]) (Set.range.{u_1, u_2 + 1} (ι := E) (minpoly F)) (Set.range.{u_1, u_3 + 1} (ι := K) (minpoly F))
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
x : E
hx : Eq (α := F[X]) (minpoly F x) (minpoly F y)
⊢ Eq (α := F[X]) (minpoly F x) 0

Tactic:
rw [minpoly.eq_zero hy] at hx

Premises used: minpoly.eq_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 : Eq (α := Set F[X]) (Set.range.{u_1, u_2 + 1} (ι := E) (minpoly F)) (Set.range.{u_1, u_3 + 1} (ι := K) (minpoly F))
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
x : E
hx : Eq (α := F[X]) (minpoly F x) 0
⊢ False

Tactic:
minpoly.ne_zero ((alg.isIntegral).1 x) hx

Premises used: Algebra.IsIntegral.isIntegral, 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 : Eq (α := Set F[X]) (Set.range.{u_1, u_2 + 1} (ι := E) (minpoly F)) (Set.range.{u_1, u_3 + 1} (ι := K) (minpoly F))
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
x : E
hx : Eq (α := F[X]) (minpoly F x) 0
⊢ False

Tactic:
exact minpoly.ne_zero ((alg.isIntegral).1 x) hx

Premises used: Algebra.IsIntegral.isIntegral, 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 :
  Subset.{u_1} (α := Set F[X]) {p : F[X] | ∃ (x : E), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)}
    {p : F[X] | ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) p : K) (0 : K)}
⊢ Nonempty (E →ₐ[F] K)

Tactic:
nonempty_algHom_of_minpoly_eq fun x ↦
    have ⟨y, hy⟩ := h ⟨_, minpoly.aeval F x⟩
    ⟨y, (minpoly.eq_iff_aeval_minpoly_eq_zero <| (alg.isIntegral).1 x).mpr hy⟩

Premises used: Iff.mpr, Algebra.IsIntegral.isIntegral, Exists, minpoly.aeval, minpoly, _private.0.Field.nonempty_algHom_of_aeval_eq_zero_subset.match_1, Exists.intro, minpoly.eq_iff_aeval_minpoly_eq_zero, Field.nonempty_algHom_of_minpoly_eq, Eq
-- 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
inst_5 : Algebra.IsAlgebraic F K
h :
  Eq.{u_1 + 1} (α := Set F[X]) {p : F[X] | ∃ (x : E), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)}
    {p : F[X] | ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) p : K) (0 : K)}
⊢ Nonempty (E ≃ₐ[F] K)

Tactic:
have ⟨σ⟩ := nonempty_algHom_of_aeval_eq_zero_subset h.le
  have ⟨τ⟩ := nonempty_algHom_of_aeval_eq_zero_subset h.ge
  ⟨.ofBijective _ (Algebra.IsAlgebraic.algHom_bijective₂ σ τ).1⟩

Premises used: Eq.ge, AlgEquiv.ofBijective, Eq.le, _private.0.Field.nonempty_algEquiv_of_range_minpoly_eq.match_2, Nonempty.intro, Algebra.IsAlgebraic.algHom_bijective₂, AlgEquiv, And.left, Nonempty, Field.nonempty_algHom_of_aeval_eq_zero_subset, _private.0.Field.nonempty_algEquiv_of_range_minpoly_eq.match_1
-- Module: Mathlib.FieldTheory.Isaacs
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
alg : Algebra.IsAlgebraic F E
h : ∀ (p : F[X]), p.Monic → Irreducible p → ∃ (x : E), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)
⊢ IsAlgClosure F E

Tactic:
.of_splits fun p _ _ ↦
    have ⟨σ⟩ := nonempty_algHom_of_exists_root fun x : p.SplittingField ↦
      have := Algebra.IsAlgebraic.isIntegral (K := F).1 x
      h _ (minpoly.monic this) (minpoly.irreducible this)
    Splits.of_algHom (SplittingField.splits _) σ

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic, Algebra.algebraMap, _private.0.IsAlgClosure.of_exists_root.match_1, Field.nonempty_algHom_of_exists_root, Polynomial.SplittingField.splits, IsAlgClosure.of_splits, minpoly, Polynomial.Splits.of_algHom, Polynomial.map, Polynomial.Splits, minpoly.irreducible
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
⊢ IsPurelyInseparable (↥k) D →
    ∀ (x : D), ∃ (n : ℕ), Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) (x ^ p ^ n)

Tactic:
have := (@isPurelyInseparable_iff_pow_mem k D _ _ _ _ p (ExpChar.expChar_center_iff.2 hchar)).1
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
this :
  IsPurelyInseparable (↥k) D →
    ∀ (x : D), ∃ (n : ℕ), Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) (x ^ p ^ n)
x : D
hx : IsSeparable (↥k) x
rw :
  ∃ (a : D) (b : Membership.mem (γ := Subring D) k a),
    (algebraMap (↥k) D : (a : ↥k) → D) (Subtype.mk (p := fun (a : D) ↦ Membership.mem (γ := Subring D) k a) a b) = x
⊢ Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) x

Tactic:
rw [RingHom.mem_range, Subtype.exists]

Premises used: RingHom.mem_range, Subtype.exists
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
this :
  IsPurelyInseparable (↥k) D →
    ∀ (x : D), ∃ (n : ℕ), Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) (x ^ p ^ n)
x : D
hx : IsSeparable (↥k) x
⊢ ∃ (a : D) (b : Membership.mem (γ := Subring D) k a),
    (algebraMap (↥k) D : (a : ↥k) → D) (Subtype.mk (p := fun (a : D) ↦ Membership.mem (γ := Subring D) k a) a b) = x

Tactic:
⟨x, ⟨hinsep x hx, rfl⟩⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
this :
  IsPurelyInseparable (↥k) D →
    ∀ (x : D), ∃ (n : ℕ), Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) (x ^ p ^ n)
x : D
hx : IsSeparable (↥k) x
⊢ ∃ (a : D) (b : Membership.mem (γ := Subring D) k a),
    (algebraMap (↥k) D : (a : ↥k) → D) (Subtype.mk (p := fun (a : D) ↦ Membership.mem (γ := Subring D) k a) a b) = x

Tactic:
exact ⟨x, ⟨hinsep x hx, rfl⟩⟩
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
this :
  IsPurelyInseparable (↥k) D →
    ∀ (x : D), ∃ (n : ℕ), Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) (x ^ p ^ n)
⊢ IsPurelyInseparable (↥k) D

Tactic:
have pure : IsPurelyInseparable k D := ⟨Algebra.IsAlgebraic.isIntegral, fun x hx ↦ by
    rw [RingHom.mem_range, Subtype.exists]
    exact ⟨x, ⟨hinsep x hx, rfl⟩⟩⟩
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
this :
  IsPurelyInseparable (↥k) D →
    ∀ (x : D), ∃ (n : ℕ), Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) (x ^ p ^ n)
pure : IsPurelyInseparable (↥k) D
obtain :
  ∀ (n : ℕ) (m : ↥k) (hm : (algebraMap (↥k) D : (a : ↥k) → D) m = a ^ p ^ n),
    ∃ (n : ℕ), Membership.mem (γ := Subring D) k (a ^ p ^ n)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring D) k (a ^ p ^ n)

Tactic:
obtain ⟨n, ⟨m, hm⟩⟩ := this pure a
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
this :
  IsPurelyInseparable (↥k) D →
    ∀ (x : D), ∃ (n : ℕ), Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) (x ^ p ^ n)
pure : IsPurelyInseparable (↥k) D
n : ℕ
m : ↥k
hm : (algebraMap (↥k) D : (a : ↥k) → D) m = a ^ p ^ n
⊢ Set.range (ι := ↥k) (⇑(algebraMap (↥k) D) : (a : ↥k) → D) ⊆
    (↑{ toSubsemiring := Subring.toSubsemiring k, algebraMap_mem' := ⋯ : Subalgebra (↥k) D } : Set D)

Tactic:
have := Subalgebra.range_subset (R := k) ⟨(k).toSubsemiring, fun r ↦ r.2⟩
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
this_1 :
  IsPurelyInseparable (↥k) D →
    ∀ (x : D), ∃ (n : ℕ), Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) (x ^ p ^ n)
pure : IsPurelyInseparable (↥k) D
n : ℕ
m : ↥k
hm : (algebraMap (↥k) D : (a : ↥k) → D) m = a ^ p ^ n
this :
  Set.range (ι := ↥k) (⇑(algebraMap (↥k) D) : (a : ↥k) → D) ⊆
    (↑{ toSubsemiring := Subring.toSubsemiring k, algebraMap_mem' := ⋯ : Subalgebra (↥k) D } : Set D)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring D) k (a ^ p ^ n)

Tactic:
⟨n, Set.mem_of_subset_of_mem this <| Set.mem_range.2 ⟨m, hm⟩⟩

Premises used: Iff.mpr, Set.mem_range, Set.mem_of_subset_of_mem, Exists.intro
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
this_1 :
  IsPurelyInseparable (↥k) D →
    ∀ (x : D), ∃ (n : ℕ), Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) (x ^ p ^ n)
pure : IsPurelyInseparable (↥k) D
n : ℕ
m : ↥k
hm : (algebraMap (↥k) D : (a : ↥k) → D) m = a ^ p ^ n
this :
  Set.range (ι := ↥k) (⇑(algebraMap (↥k) D) : (a : ↥k) → D) ⊆
    (↑{ toSubsemiring := Subring.toSubsemiring k, algebraMap_mem' := ⋯ : Subalgebra (↥k) D } : Set D)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring D) k (a ^ p ^ n)

Tactic:
exact ⟨n, Set.mem_of_subset_of_mem this <| Set.mem_range.2 ⟨m, hm⟩⟩