awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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
⊢ ∃ (i : Ω), Subtype.mk (p := fun (x : E) ↦ x ∈ FS) α hα ∈ (↑(M i) : Set ↥FS)
have 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)
Tactic: have ⟨β, hβ⟩ := h α
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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 α)))
⊢ ∃ (i : Ω), Subtype.mk (p := fun (x : E) ↦ x ∈ FS) α hα ∈ (↑(M i) : Set ↥FS)
have have : ∀ (ω : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K') (hω : ω.comp (inclusion sorry) = ϕ),
  ∃ (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α)
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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)
have refine : Eq.{u_3 + 1} (α := K') ((ϕ : (a : ↥F⟮α⟯) → K') (AdjoinSimple.gen F α) : K')
  ((AlgHom.toRingHom (Algebra.ofId K K') : (a : K) → K') β : K')
Tactic: refine ⟨ω, β, ((DFunLike.congr_fun hω <| AdjoinSimple.gen F α).trans ?_).symm⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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.{u_3 + 1} (α := K') ((ϕ : (a : ↥F⟮α⟯) → K') (AdjoinSimple.gen F α) : K')
    ((AlgHom.toRingHom (Algebra.ofId K K') : (a : K) → K') β : K')
have rw : Eq (α := K') ((IsScalarTower.toAlgHom F K K' : (a : K) → K') β : 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (hypothesis)
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
⊢ AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
have this₁ : 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
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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 ω
have inl : Finite F → ∃ (ω : Ω), ⊤ ≤ M ω
Tactic: cases finite_or_infinite F
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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 ω
⊢ ∃ (ω : Ω), ⊤ ≤ M ω
have inr : Infinite F → ∃ (ω : Ω), ⊤ ≤ M ω
Tactic: cases finite_or_infinite F
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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
⊢ ∃ (ω : Ω), ⊤ ≤ M ω
have inl : ∀ (α : ↥FS) (hα : Eq (α := IntermediateField F ↥FS) F⟮α⟯ ⊤), ∃ (ω : Ω), ⊤ ≤ M ω
Tactic: have ⟨α, hα⟩ := exists_primitive_element_of_finite_bot F FS
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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⟮α⟯ ⊤
⊢ ∃ (ω : Ω), ⊤ ≤ M ω
have inl : ∀ (ω : Ω) (hω : α ∈ (↑(M ω) : Set ↥FS)), ∃ (ω : Ω), ⊤ ≤ M ω
Tactic: have ⟨ω, hω⟩ := Set.mem_iUnion.mp (this ▸ Set.mem_univ α)
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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)
⊢ ⊤ ≤ comap ω K₀
have rwa : F⟮α⟯ ≤ comap ω K₀
Tactic: rwa [← hα, adjoin_simple_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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₀
⊢ ⊤ ≤ comap ω K₀
have rwa₁ : α ∈ comap ω K₀
Tactic: rwa [← hα, adjoin_simple_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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
⊢ ∃ (ω : Ω), ⊤ ≤ M ω
have inr : ∃ (ω : Ω), M ω = ⊤
Tactic: simp_rw [top_le_iff, Subspace.exists_eq_top_of_iUnion_eq_univ this]
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (hypothesis)
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
⊢ AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
have ω : ∃ (ω : Ω), ⊤ ≤ 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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)
⊢ Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
have rw : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F y) : K) (0 : K)
Tactic: rw [hy, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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)
⊢ Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
have rw₁ : Eq.{u_3 + 1} (α := K) 0 0
Tactic: rw [hy, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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
⊢ IsIntegral F y
have by_contra : ∀ (hy : ¬IsIntegral F y), False
Tactic: by_contra hy
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
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
⊢ False
have have : ∀ (x : E) (hx : Eq (α := F[X]) (minpoly F x) (minpoly F y)), False
Tactic: have ⟨x, hx⟩ := h.ge ⟨y, rfl⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (hypothesis)
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)
⊢ False
have hx₁ : Eq (α := F[X]) (minpoly F x) 0
Tactic: rw [minpoly.eq_zero hy] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
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
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring D) k (a ^ p ^ n)
have this : 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
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
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
⊢ Membership.mem (γ := Subring D) (RingHom.range (R := ↥k) (algebraMap (↥k) D)) x
have 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
Tactic: rw [RingHom.mem_range, Subtype.exists]
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
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)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring D) k (a ^ p ^ n)
have pure : 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⟩⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
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 : ℕ), Membership.mem (γ := Subring D) k (a ^ p ^ n)
have obtain : ∀ (n : ℕ) (m : ↥k) (hm : (algebraMap (↥k) D : (a : ↥k) → D) m = a ^ p ^ n),
  ∃ (n : ℕ), Membership.mem (γ := Subring D) k (a ^ p ^ n)
Tactic: obtain ⟨n, ⟨m, hm⟩⟩ := this pure a
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
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
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring D) k (a ^ p ^ n)
have this₁ : Set.range (ι := ↥k) (⇑(algebraMap (↥k) D) : (a : ↥k) → D) ⊆
  (↑{ toSubsemiring := Subring.toSubsemiring k, algebraMap_mem' := sorry : Subalgebra (↥k) D } : Set D)
Tactic: have := Subalgebra.range_subset (R := k) ⟨(k).toSubsemiring, fun r ↦ r.2⟩