awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p) ∧
    Splits (R := (p * minpoly F x).SplittingField)
      (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have hL2 : Splits (R := (p * minpoly F x).SplittingField)
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))
Tactic: obtain ⟨hL1, hL2⟩ := hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
hL2 :
  Splits (R := (p * minpoly F x).SplittingField)
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have hL2₁ : Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
Tactic: rw [← j.comp_algebraMap, ← Polynomial.map_map] at hL2
Cleared hypotheses: hL2
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have inr : ∀ (a : L) (ha : a ∈ roots (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))),
  Membership.mem (γ := Subring L) (RingHom.range (↑j : E →+* L)) a
Tactic: refine ⟨hx, Splits.of_splits_map (j : E →+* L) hL2 fun a ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
a : L
ha : a ∈ roots (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
⊢ Membership.mem (γ := Subring L) (RingHom.range (↑j : E →+* L)) a
have ha₁ : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
Tactic: rw [Polynomial.map_map, j.comp_algebraMap] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this_1 : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra.{u_3, u_1} (↥F⟮x⟯) L :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := F)
      ((Equiv.symm (algHomAdjoinIntegralEquiv F hx) : (a : { x_1 : L // x_1 ∈ (minpoly F x).aroots L }) → ↥F⟮x⟯ →ₐ[F] L)
        (Subtype.mk (p := fun (x_1 : L) ↦ x_1 ∈ aroots (minpoly F x) L) a ha)))
inr : Membership.mem (γ := Subring L) (RingHom.range (↑j : E →+* L)) a
⊢ Membership.mem (γ := Subring L) (RingHom.range (↑j : E →+* L)) a
have inr₁ : (Polynomial.map.{u_3, u_1} (R := ↥F⟮x⟯) (algebraMap (↥F⟮x⟯) L) (Polynomial.map (algebraMap F ↥F⟮x⟯) p)).Splits
Tactic: let j' : E →ₐ[F⟮x⟯] L := IsSplittingField.lift E (p.map (algebraMap F F⟮x⟯)) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this_1 : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra.{u_3, u_1} (↥F⟮x⟯) L :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := F)
      ((Equiv.symm (algHomAdjoinIntegralEquiv F hx) : (a : { x_1 : L // x_1 ∈ (minpoly F x).aroots L }) → ↥F⟮x⟯ →ₐ[F] L)
        (Subtype.mk (p := fun (x_1 : L) ↦ x_1 ∈ aroots (minpoly F x) L) a ha)))
j' : E →ₐ[↥F⟮x⟯] L := IsSplittingField.lift E (Polynomial.map (algebraMap F ↥F⟮x⟯) p) ⋯
⊢ Membership.mem (γ := Subring L) (RingHom.range (↑j : E →+* L)) a
have inr : a ∈ j.range
Tactic: change a ∈ j.range
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this_1 : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra.{u_3, u_1} (↥F⟮x⟯) L :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := F)
      ((Equiv.symm (algHomAdjoinIntegralEquiv F hx) : (a : { x_1 : L // x_1 ∈ (minpoly F x).aroots L }) → ↥F⟮x⟯ →ₐ[F] L)
        (Subtype.mk (p := fun (x_1 : L) ↦ x_1 ∈ aroots (minpoly F x) L) a ha)))
j' : E →ₐ[↥F⟮x⟯] L := IsSplittingField.lift E (Polynomial.map (algebraMap F ↥F⟮x⟯) p) ⋯
⊢ a ∈ j.range
have inr : Membership.mem (γ := Subalgebra F L) (AlgHom.range (AlgHom.restrictScalars F j')) a
Tactic: rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
            IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this_1 : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra.{u_3, u_1} (↥F⟮x⟯) L :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := F)
      ((Equiv.symm (algHomAdjoinIntegralEquiv F hx) : (a : { x_1 : L // x_1 ∈ (minpoly F x).aroots L }) → ↥F⟮x⟯ →ₐ[F] L)
        (Subtype.mk (p := fun (x_1 : L) ↦ x_1 ∈ aroots (minpoly F x) L) a ha)))
⊢ (Polynomial.map.{u_3, u_1} (R := ↥F⟮x⟯) (algebraMap (↥F⟮x⟯) L) (Polynomial.map (algebraMap F ↥F⟮x⟯) p)).Splits
have inr : (Polynomial.map
    (@RingHom.comp.{u_1, u_3, u_1} _ ↥F⟮x⟯ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥F⟮x⟯) L)
      (algebraMap F ↥F⟮x⟯))
    p).Splits
Tactic: rwa [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
⊢ Normal.{u_1, u_2} F ↥(⨆ (i : ι), t i)
have refine : ∀ (x : ↥(⨆ (i : ι), t i)),
  Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
Tactic: refine { toIsAlgebraic := isAlgebraic_iSup fun i => (h i).1, splits' := fun x => ?_ }
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
⊢ Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
have obtain : ∀ (s : Finset ((i : ι) × ↥(t i)))
  (hx :
    Membership.mem (γ := IntermediateField F K)
      (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)),
  Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
Tactic: obtain ⟨s, hx⟩ := exists_finset_of_mem_supr'' (fun i => (h i).1) x.2
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
⊢ IsSplittingField.{u_1, u_2} F (↥E) (∏ i ∈ s, minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i))))
have refine_1 : Ne.{u_1 + 1} (α := F[X]) (∏ i ∈ s, minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) 0
Tactic: refine isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
refine_1 : Ne.{u_1 + 1} (α := F[X]) (∏ i ∈ s, minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) 0
⊢ IsSplittingField.{u_1, u_2} F (↥E) (∏ i ∈ s, minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i))))
have refine_2 : ∀ i ∈ s, Splits (Polynomial.map (algebraMap F K) (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))))
Tactic: refine isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
⊢ Normal.{u_1, u_2} F ↥E
have this : IsSplittingField.{u_1, u_2} F (↥E) (∏ i ∈ s, minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i))))
Tactic: haveI : IsSplittingField F E (∏ i ∈ s, minpoly F i.snd) := by
      refine isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_
      · exact Finset.prod_ne_zero_iff.mpr fun i _ => minpoly.ne_zero ((h i.1).isIntegral i.2)
      · simpa [Polynomial.map_map] using ((h i.1).splits i.2).map (algebraMap (t i.1) K)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
⊢ Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
have hF : Normal.{u_1, u_2} F ↥E
Tactic: have hF : Normal F E := by
    haveI : IsSplittingField F E (∏ i ∈ s, minpoly F i.snd) := by
      refine isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_
      · exact Finset.prod_ne_zero_iff.mpr fun i _ => minpoly.ne_zero ((h i.1).isIntegral i.2)
      · simpa [Polynomial.map_map] using ((h i.1).splits i.2).map (algebraMap (t i.1) K)
    apply Normal.of_isSplittingField (∏ i ∈ s, minpoly F i.2)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
⊢ E ≤ ⨆ (i : ι), t i
have refine : ∀ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K) ≤ t (i.fst (β := fun (i : ι) ↦ ↥(t i)))
Tactic: refine iSup_le fun i => iSup_le fun _ => le_iSup_of_le i.1 ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
i : (i : ι) × ↥(t i)
h_1 : i ∈ s
⊢ adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K) ≤ t (i.fst (β := fun (i : ι) ↦ ↥(t i)))
have rw : Set.image (α := ↥(t (i.fst (β := fun (i : ι) ↦ ↥(t i)))))
    (⇑(t (i.fst (β := fun (i : ι) ↦ ↥(t i)))).val : (a : ↥(t i.fst)) → K)
    (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) ↥(t (i.fst (β := fun (i : ι) ↦ ↥(t i))))) ⊆
  (↑(t (i.fst (β := fun (i : ι) ↦ ↥(t i)))) : Set K)
Tactic: rw [adjoin_le_iff, ← ((h i.1).splits i.2).image_rootSet (t i.1).val]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
⊢ Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
have hE : E ≤ ⨆ (i : ι), t i
Tactic: have hE : E ≤ ⨆ i, t i := by
    refine iSup_le fun i => iSup_le fun _ => le_iSup_of_le i.1 ?_
    rw [adjoin_le_iff, ← ((h i.1).splits i.2).image_rootSet (t i.1).val]
    exact fun _ ⟨a, _, h⟩ => h ▸ a.2
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
hE : E ≤ ⨆ (i : ι), t i
⊢ Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
have this : Splits.{u_2} (R := ↥E)
  (Polynomial.map (algebraMap F ↥E) (minpoly F (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (↑x : K) hx)))
Tactic: have := hF.splits ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
hE : E ≤ ⨆ (i : ι), t i
this :
  Splits.{u_2} (R := ↥E)
    (Polynomial.map (algebraMap F ↥E) (minpoly F (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (↑x : K) hx)))
⊢ Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
have this₁ : Splits.{u_2} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
Tactic: rw [minpoly_eq, Subtype.coe_mk, ← minpoly_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
hE : E ≤ ⨆ (i : ι), t i
this : Splits.{u_2} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
⊢ Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
have this₁ : (Polynomial.map (inclusion hE).toRingHom (Polynomial.map (algebraMap F ↥E) (minpoly F x))).Splits
Tactic: have := this.map (inclusion hE).toRingHom
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
hE : E ≤ ⨆ (i : ι), t i
this_1 : Splits.{u_2} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
this : (Polynomial.map (inclusion hE).toRingHom (Polynomial.map (algebraMap F ↥E) (minpoly F x))).Splits
⊢ Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
have rwa : ∀ (this : (Polynomial.map ((inclusion hE).comp (algebraMap F ↥E)) (minpoly F x)).Splits),
  Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
Tactic: rwa [Polynomial.map_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have normal : Normal.{u_1, u_3} F ↥E
Tactic: have normal : Normal F E := normal_iSup (h := fun x ↦
    Normal.of_isSplittingField (hFEp := adjoin_rootSet_isSplittingField (splits x x.2).2))
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have this : ∀ x ∈ S, Splits.{u_3} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
Tactic: have : ∀ x ∈ S, ((minpoly F x).map (algebraMap F E)).Splits := fun x hx ↦ splits_of_splits
    (splits x hx).2 fun y hy ↦ (le_iSup _ ⟨x, hx⟩ : _ ≤ E) (subset_adjoin F _ <| by exact hy)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
this : ∀ x ∈ S, Splits.{u_3} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have obtain : ∀ (φ : AlgHom.{u_1, u_2, u_3} F ↥(adjoin F S) ↥E), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
Tactic: obtain ⟨φ⟩ := nonempty_algHom_adjoin_of_splits fun x hx ↦ ⟨(splits x hx).1, this x hx⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
this : ∀ x ∈ S, Splits.{u_3} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
φ : AlgHom.{u_1, u_2, u_3} F ↥(adjoin F S) ↥E
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have h : Polynomial.map (algebraMap F L) (minpoly F x) =
  Polynomial.map E.val.toRingHom
    (Polynomial.map (algebraMap F ↥E)
      (minpoly.{u_1, u_3} F (B := ↥E)
        ((φ : (a : ↥(adjoin F S)) → ↥E)
            (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := IntermediateField F K) (adjoin F S) x) x hx) :
          ↥E)))
Tactic: convert! (normal.splits <| φ ⟨x, hx⟩).map E.val.toRingHom
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
⊢ Normal.{u_1, u_2} F ↥(⨅ (i : ι), t i)
have refine_1 : Algebra.IsAlgebraic.{u_1, u_2} F ↥(⨅ (i : ι), t i)
Tactic: refine { toIsAlgebraic := ?_, splits' := fun x => ?_ }