awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Normal.Basic
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)))
⊢ a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots

Tactic:
rw [Polynomial.map_map, j.comp_algebraMap] at ha

Premises used: AlgHom.comp_algebraMap, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Normal.Basic
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
inr₁ : (Polynomial.map.{u_3, u_1} (R := ↥F⟮x⟯) (algebraMap (↥F⟮x⟯) L) (Polynomial.map (algebraMap F ↥F⟮x⟯) p)).Splits
⊢ Membership.mem (γ := Subring L) (RingHom.range (↑j : E →+* L)) a

Tactic:
let j' : E →ₐ[F⟮x⟯] L := IsSplittingField.lift E (p.map (algebraMap F F⟮x⟯)) ?_
-- Module: Mathlib.FieldTheory.Normal.Basic
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) ⋯
inr : a ∈ j.range
⊢ Membership.mem (γ := Subring L) (RingHom.range (↑j : E →+* L)) a

Tactic:
change a ∈ j.range

Premises used: AlgHom.range
-- Module: Mathlib.FieldTheory.Normal.Basic
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) ⋯
inr : Membership.mem (γ := Subalgebra F L) (AlgHom.range (AlgHom.restrictScalars F j')) a
⊢ a ∈ j.range

Tactic:
rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
            IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]

Premises used: AlgHom.restrictScalars, Polynomial.IsSplittingField.adjoin_rootSet_eq_range
-- Module: Mathlib.FieldTheory.Normal.Basic
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 (γ := Subalgebra F L) (AlgHom.range (AlgHom.restrictScalars F j')) a

Tactic:
⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩

Premises used: Set.Mem, setOf, IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen, AlgHom.commutes, Exists.intro, Set.range, Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Basic
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 (γ := Subalgebra F L) (AlgHom.range (AlgHom.restrictScalars F j')) a

Tactic:
exact ⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩
-- Module: Mathlib.FieldTheory.Normal.Basic
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 :
  (Polynomial.map
      (@RingHom.comp.{u_1, u_3, u_1} _ ↥F⟮x⟯ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥F⟮x⟯) L)
        (algebraMap F ↥F⟮x⟯))
      p).Splits
inr₁ inr₂ inr₃ inr₄ : (Polynomial.map (algebraMap F L) p).Splits
⊢ (Polynomial.map.{u_3, u_1} (R := ↥F⟮x⟯) (algebraMap (↥F⟮x⟯) L) (Polynomial.map (algebraMap F ↥F⟮x⟯) p)).Splits

Tactic:
rwa [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Normal.Basic
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 :
  (HMul.hMul (α := (p * minpoly F x).SplittingField[X])
      (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
      (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))).Splits
⊢ Ne (α := (p * minpoly F x).SplittingField[X]) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p) 0

Tactic:
Polynomial.map_ne_zero hp

Premises used: Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.Normal.Basic
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 :
  (HMul.hMul (α := (p * minpoly F x).SplittingField[X])
      (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
      (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))).Splits
⊢ Ne (α := (p * minpoly F x).SplittingField[X]) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p) 0

Tactic:
exact Polynomial.map_ne_zero hp

Premises used: Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : Type u_3
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
p : F[X]
⊢ Normal F p.SplittingField

Tactic:
Normal.of_isSplittingField p

Premises used: Normal.of_isSplittingField
-- Module: Mathlib.FieldTheory.Normal.Basic
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)

Tactic:
{ toIsAlgebraic := isAlgebraic_iSup fun i => (h i).1, splits' := fun x => ?_ }

Premises used: Normal.mk, Normal.toIsAlgebraic, IntermediateField.isAlgebraic_iSup
-- Module: Mathlib.FieldTheory.Normal.Basic
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)
refine :
  ∀ (x : ↥(⨆ (i : ι), t i)),
    Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
⊢ Normal.{u_1, u_2} F ↥(⨆ (i : ι), t i)

Tactic:
refine { toIsAlgebraic := isAlgebraic_iSup fun i => (h i).1, splits' := fun x => ?_ }
-- Module: Mathlib.FieldTheory.Normal.Basic
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)
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))
⊢ 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

Premises used: IntermediateField.exists_finset_of_mem_supr'', Normal.toIsAlgebraic, Subtype.property
-- Module: Mathlib.FieldTheory.Normal.Basic
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))))

Tactic:
isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_

Premises used: Set.Mem, IntermediateField.isSplittingField_iSup, IntermediateField.adjoin_rootSet_isSplittingField
-- Module: Mathlib.FieldTheory.Normal.Basic
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
refine_2 : ∀ i ∈ s, Splits (Polynomial.map (algebraMap F K) (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))))
⊢ IsSplittingField.{u_1, u_2} F (↥E) (∏ i ∈ s, minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i))))

Tactic:
refine isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_

Premises used: IntermediateField.isSplittingField_iSup, IntermediateField.adjoin_rootSet_isSplittingField
-- Module: Mathlib.FieldTheory.Normal.Basic
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)
⊢ Ne.{u_1 + 1} (α := F[X]) (∏ i ∈ s, minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) 0

Tactic:
Finset.prod_ne_zero_iff.mpr fun i _ => minpoly.ne_zero ((h i.1).isIntegral i.2)

Premises used: Iff.mpr, Sigma.fst, Finset.prod_ne_zero_iff, Normal.isIntegral, Sigma.snd, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Basic
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)
⊢ Ne.{u_1 + 1} (α := F[X]) (∏ i ∈ s, minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) 0

Tactic:
exact Finset.prod_ne_zero_iff.mpr fun i _ => minpoly.ne_zero ((h i.1).isIntegral i.2)

Premises used: Iff.mpr, Finset.prod_ne_zero_iff, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Basic
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)
i : (i : ι) × ↥(t i)
h_1 : i ∈ s
⊢ Splits (Polynomial.map (algebraMap F K) (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))))

Tactic:
simpa [Polynomial.map_map] using ((h i.1).splits i.2).map (algebraMap (t i.1) K)

Premises used: Algebra.algebraMap, Normal.splits, Membership.mem, Subtype, Sigma.fst, Polynomial.Splits.map, Polynomial.map_map, Sigma.snd
-- Module: Mathlib.FieldTheory.Normal.Basic
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))))

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)
-- Module: Mathlib.FieldTheory.Normal.Basic
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)
this : IsSplittingField.{u_1, u_2} F (↥E) (∏ i ∈ s, minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i))))
⊢ Normal.{u_1, u_2} F ↥E

Tactic:
apply Normal.of_isSplittingField (∏ i ∈ s, minpoly F i.2)

Premises used: Normal.of_isSplittingField, minpoly, Finset.prod, Sigma.snd
-- Module: Mathlib.FieldTheory.Normal.Basic
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

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)
-- Module: Mathlib.FieldTheory.Normal.Basic
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

Tactic:
iSup_le fun i => iSup_le fun _ => le_iSup_of_le i.1 ?_

Premises used: Set.Mem, setOf, Sigma.fst, le_iSup_of_le, iSup_le
-- Module: Mathlib.FieldTheory.Normal.Basic
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
refine :
  ∀ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K) ≤ t (i.fst (β := fun (i : ι) ↦ ↥(t i)))
⊢ E ≤ ⨆ (i : ι), t i

Tactic:
refine iSup_le fun i => iSup_le fun _ => le_iSup_of_le i.1 ?_

Premises used: le_iSup_of_le, iSup_le
-- Module: Mathlib.FieldTheory.Normal.Basic
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
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)
⊢ adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K) ≤ t (i.fst (β := fun (i : ι) ↦ ↥(t i)))

Tactic:
rw [adjoin_le_iff, ← ((h i.1).splits i.2).image_rootSet (t i.1).val]

Premises used: IntermediateField.adjoin_le_iff, Normal.splits, Sigma.fst, Polynomial.Splits.image_rootSet, IntermediateField.val, Sigma.snd
-- Module: Mathlib.FieldTheory.Normal.Basic
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
⊢ 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:
fun _ ⟨a, _, h⟩ => h ▸ a.2

Premises used: Membership.mem, Eq.rec, Sigma.fst, Set.Subset, SetLike.coe, _private.0.IntermediateField.normal_iSup.match_1, Subtype.property
-- Module: Mathlib.FieldTheory.Normal.Basic
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
⊢ 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:
exact fun _ ⟨a, _, h⟩ => h ▸ a.2
-- Module: Mathlib.FieldTheory.Normal.Basic
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

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