awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ LE.le.{u_3} (α := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤
    (⨆ (f : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)), f.fieldRange)

Tactic:
fun x _ ↦ ((⨆ f : K →ₐ[F] L, f.fieldRange).val).injective.mem_set_image |>.mp ?_

Premises used: iSup, RingHom.injective, AlgHom.fieldRange, AlgHom.toRingHom, Iff.mp, IntermediateField.val, Function.Injective.mem_set_image
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
right :
  ∀ (x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
    Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x →
      Membership.mem (α := L) (γ := Set L)
        ((⇑(AlgHom.toRingHom (val (⨆ (f : K →ₐ[F] L), f.fieldRange))) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) ''
          (↑(⨆ (f : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)), f.fieldRange) :
            Set ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)))
        ((AlgHom.toRingHom (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) x :
          L)
⊢ LE.le.{u_3} (α := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤
    (⨆ (f : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)), f.fieldRange)

Tactic:
refine fun x _ ↦ ((⨆ f : K →ₐ[F] L, f.fieldRange).val).injective.mem_set_image |>.mp ?_

Premises used: iSup, RingHom.injective, AlgHom.fieldRange, AlgHom.toRingHom, Iff.mp, IntermediateField.val, Function.Injective.mem_set_image
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)
h : Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x
right :
  Membership.mem (α := L)
    (↑(⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
          IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange) :
      Set L)
    ((val (⨆ (f : K →ₐ[F] L), f.fieldRange) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) x : L)
⊢ Membership.mem (α := L) (γ := Set L)
    ((⇑(AlgHom.toRingHom (val (⨆ (f : K →ₐ[F] L), f.fieldRange))) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) ''
      (↑(⨆ (f : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)), f.fieldRange) :
        Set ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)))
    ((AlgHom.toRingHom (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) x : L)

Tactic:
rw [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, coe_val, ← IntermediateField.coe_val,
    ← IntermediateField.coe_map, IntermediateField.map_iSup]

Premises used: RingHom.coe_coe, IntermediateField.coe_val, IntermediateField.map_iSup, AlgHom.toRingHom_eq_coe, IntermediateField.coe_map
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)
h : Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x
⊢ Membership.mem (α := L)
    (↑(⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
          IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange) :
      Set L)
    ((val (⨆ (f : K →ₐ[F] L), f.fieldRange) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) x : L)

Tactic:
(iSup_le fun f ↦ ?_ : normalClosure F K L ≤ _) x.2

Premises used: iSup_le, Subtype.property
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)
h : Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x
right :
  ∀ (f : K →ₐ[F] L),
    f.fieldRange ≤
      ⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
        IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange
⊢ Membership.mem (α := L)
    (↑(⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
          IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange) :
      Set L)
    ((val (⨆ (f : K →ₐ[F] L), f.fieldRange) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) x : L)

Tactic:
refine (iSup_le fun f ↦ ?_ : normalClosure F K L ≤ _) x.2

Premises used: iSup_le, Subtype.property
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)
h : Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x
f : K →ₐ[F] L
⊢ f.fieldRange ≤
    ⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
      IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange

Tactic:
le_iSup_of_le (f.codRestrict _ fun x ↦ f.fieldRange_le_normalClosure ⟨x, rfl⟩) ?_

Premises used: Set.Mem, le_iSup_of_le, Exists.intro, AlgHom.fieldRange_le_normalClosure, AlgHom.codRestrict, rfl
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)
h : Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x
f : K →ₐ[F] L
right :
  f.fieldRange ≤
    IntermediateField.map (L := ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) (val (⨆ (f : K →ₐ[F] L), f.fieldRange))
      (AlgHom.fieldRange (f.codRestrict (toSubalgebra (⨆ (f : K →ₐ[F] L), f.fieldRange)) ⋯))
⊢ f.fieldRange ≤
    ⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
      IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange

Tactic:
refine le_iSup_of_le (f.codRestrict _ fun x ↦ f.fieldRange_le_normalClosure ⟨x, rfl⟩) ?_

Premises used: le_iSup_of_le, Exists.intro, AlgHom.fieldRange_le_normalClosure, AlgHom.codRestrict, rfl
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
⊢ Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L)) ⊤

Tactic:
have := h.adjoin_rootSet
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L)) ⊤
⊢ Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤

Tactic:
rw [← gc.l_iSup] at this

Premises used: GaloisConnection.l_iSup, IntermediateField.gc
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
refine :
  ∀ (x : L) (hx : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x),
    Splits (Polynomial.map (algebraMap F L') (minpoly F x))
⊢ L →ₐ[F] L'

Tactic:
refine Nonempty.some <| nonempty_algHom_of_adjoin_splits
    (fun x hx ↦ ⟨isAlgebraic_iff_isIntegral.mp ((h.normal).isAlgebraic x), ?_⟩) this

Premises used: Algebra.IsAlgebraic.isAlgebraic, Nonempty.some, And.intro, Iff.mp, IntermediateField.nonempty_algHom_of_adjoin_splits, isAlgebraic_iff_isIntegral
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
x : L
hx : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x
obtain : ∀ (y : K) (hx : x ∈ rootSet (minpoly F y) L), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
⊢ Splits (Polynomial.map (algebraMap F L') (minpoly F x))

Tactic:
obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
x : L
hx_1 : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x
y : K
hx : x ∈ rootSet (minpoly F y) L
pos : ∀ (iy : IsIntegral F y), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
neg : ∀ (iy : ¬IsIntegral F y), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
⊢ Splits (Polynomial.map (algebraMap F L') (minpoly F x))

Tactic:
by_cases iy : IsIntegral F y

Premises used: IsIntegral
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
x : L
hx_1 : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x
y : K
hx : x ∈ rootSet (minpoly F y) L
iy : IsIntegral F y
⊢ Splits (Polynomial.map (algebraMap F L') (minpoly F x))

Tactic:
(splits y).of_dvd (map_ne_zero (minpoly.ne_zero iy))
      ((map_dvd_map' _).mpr (minpoly.dvd F x (mem_rootSet.mp hx).2))

Premises used: Iff.mpr, And.right, Iff.mp, Polynomial.mem_rootSet, Polynomial.Splits.of_dvd, minpoly.dvd, Polynomial.map_ne_zero, Polynomial.map_dvd_map', minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
x : L
hx_1 : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x
y : K
hx : x ∈ rootSet (minpoly F y) L
iy : IsIntegral F y
⊢ Splits (Polynomial.map (algebraMap F L') (minpoly F x))

Tactic:
exact (splits y).of_dvd (map_ne_zero (minpoly.ne_zero iy))
      ((map_dvd_map' _).mpr (minpoly.dvd F x (mem_rootSet.mp hx).2))

Premises used: Iff.mpr, And.right, Iff.mp, Polynomial.mem_rootSet, Polynomial.Splits.of_dvd, minpoly.dvd, Polynomial.map_ne_zero, Polynomial.map_dvd_map', minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
x : L
hx_1 : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x
y : K
hx : x ∈ rootSet (minpoly F y) L
iy : ¬IsIntegral F y
⊢ Splits (Polynomial.map (algebraMap F L') (minpoly F x))

Tactic:
simp [minpoly.eq_zero iy] at hx

Premises used: minpoly.eq_zero
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
have : ∀ (φ : K →ₐ[F] L), IsNormalClosure.{u_1, u_2, u_3} F K ↥(normalClosure F K L)
⊢ IsNormalClosure.{u_1, u_2, u_3} F K ↥(normalClosure F K L)

Tactic:
have ⟨φ⟩ := ne
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
apply : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ IsNormalClosure.{u_1, u_2, u_3} F K ↥(normalClosure F K L)

Tactic:
apply (h.toIsAlgebraic.of_injective φ φ.injective).isNormalClosure_normalClosure

Premises used: Algebra.IsAlgebraic.isNormalClosure_normalClosure
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
simp_rw : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly.{u_1, u_3} F (B := L) ((φ : (a : K) → L) x : L)))
⊢ ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))

Tactic:
simp_rw [← minpoly.algHom_eq _ φ.injective]

Premises used: minpoly.algHom_eq, RingHom.injective, AlgHom.toRingHom
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly.{u_1, u_3} F (B := L) ((φ : (a : K) → L) x : L)))

Tactic:
fun _ ↦ h.splits _

Premises used: Normal.splits, DFunLike.coe
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly.{u_1, u_3} F (B := L) ((φ : (a : K) → L) x : L)))

Tactic:
exact fun _ ↦ h.splits _

Premises used: Normal.splits
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
have :
  ∀ (φ : K →ₐ[F] L),
    Eq (α := IntermediateField F L) (normalClosure F K L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L))
⊢ Eq (α := IntermediateField F L) (normalClosure F K L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L))

Tactic:
have ⟨φ⟩ := ne
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ Eq (α := IntermediateField F L) (normalClosure F K L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L))

Tactic:
h.toIsAlgebraic.of_injective φ φ.injective
    |>.normalClosure_eq_iSup_adjoin_of_splits fun x ↦ ?_

Premises used: Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
refine : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ Eq (α := IntermediateField F L) (normalClosure F K L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L))

Tactic:
refine h.toIsAlgebraic.of_injective φ φ.injective
    |>.normalClosure_eq_iSup_adjoin_of_splits fun x ↦ ?_

Premises used: Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
rw : Splits (Polynomial.map (algebraMap F L) (minpoly.{u_1, u_3} F (B := L) ((φ : (a : K) → L) x : L)))
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))

Tactic:
rw [← minpoly.algHom_eq _ φ.injective]

Premises used: minpoly.algHom_eq, RingHom.injective, AlgHom.toRingHom
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly.{u_1, u_3} F (B := L) ((φ : (a : K) → L) x : L)))

Tactic:
apply h.splits

Premises used: Normal.splits
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra K L
inst_6 : IsScalarTower F K L
inst_7 : Normal F L
⊢ Eq (α := IntermediateField F L) (normalClosure F K L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L))

Tactic:
normalClosure_eq_iSup_adjoin' (ne := ⟨IsScalarTower.toAlgHom F K L⟩)

Premises used: normalClosure_eq_iSup_adjoin'
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : Normal F L
inl : IsEmpty (K →ₐ[F] L) → Normal.{u_1, u_3} F ↥(normalClosure F K L)
inr : ∀ (φ : Nonempty (K →ₐ[F] L)), Normal.{u_1, u_3} F ↥(normalClosure F K L)
⊢ Normal.{u_1, u_3} F ↥(normalClosure F K L)

Tactic:
obtain _ | φ := isEmpty_or_nonempty (K →ₐ[F] L)

Premises used: AlgHom, isEmpty_or_nonempty
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : Normal F L
h_1 : IsEmpty (K →ₐ[F] L)
inl : Normal.{u_1, u_3} F ↥⊥
⊢ Normal.{u_1, u_3} F ↥(normalClosure F K L)

Tactic:
rw [normalClosure, iSup_of_empty]

Premises used: IntermediateField.normalClosure, iSup_of_empty
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : Normal F L
h_1 : IsEmpty (K →ₐ[F] L)
⊢ Normal.{u_1, u_3} F ↥⊥

Tactic:
Normal.of_algEquiv (botEquiv F L).symm

Premises used: AlgEquiv.symm, Normal.of_algEquiv, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : Normal F L
h_1 : IsEmpty (K →ₐ[F] L)
⊢ Normal.{u_1, u_3} F ↥⊥

Tactic:
exact Normal.of_algEquiv (botEquiv F L).symm

Premises used: AlgEquiv.symm, Normal.of_algEquiv, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : Normal F L
φ : Nonempty (K →ₐ[F] L)
⊢ Normal.{u_1, u_3} F ↥(normalClosure F K L)

Tactic:
(isNormalClosure_normalClosure F K L).normal

Premises used: IsNormalClosure.normal
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : Normal F L
φ : Nonempty (K →ₐ[F] L)
⊢ Normal.{u_1, u_3} F ↥(normalClosure F K L)

Tactic:
exact (isNormalClosure_normalClosure F K L).normal

Premises used: IsNormalClosure.normal
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : FiniteDimensional F K
⊢ ∀ (f : K →ₐ[F] L), FiniteDimensional.{u_1, u_3} F ↥f.fieldRange

Tactic:
haveI : ∀ f : K →ₐ[F] L, FiniteDimensional F f.fieldRange := fun f ↦
    f.toLinearMap.finiteDimensional_range
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : FiniteDimensional F K
this : ∀ (f : K →ₐ[F] L), FiniteDimensional.{u_1, u_3} F ↥f.fieldRange
⊢ FiniteDimensional.{u_1, u_3} F ↥(normalClosure F K L)

Tactic:
apply IntermediateField.finiteDimensional_iSup_of_finite

Premises used: IntermediateField.finiteDimensional_iSup_of_finite
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra K L
inst_6 : IsScalarTower F K L
h :
  Eq (α := RingHom.{u_1, u_3} F ↥(normalClosure F K L)) (algebraMap F ↥(normalClosure F K L))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K ↥(normalClosure F K L)) (algebraMap F K))
⊢ IsScalarTower.{u_1, u_2, u_3} F K ↥(normalClosure F K L)

Tactic:
apply of_algebraMap_eq'

Premises used: IsScalarTower.of_algebraMap_eq'
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra K L
inst_6 : IsScalarTower F K L
h :
  ∀ (x : F),
    Eq.{u_3 + 1} (α := L) (↑((algebraMap F ↥(normalClosure F K L) : (a : F) → ↥(normalClosure F K L)) x) : L)
      (↑((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K ↥(normalClosure F K L)) (algebraMap F K) :
              (a : F) → ↥(normalClosure F K L))
            x) :
        L)
⊢ Eq (α := RingHom.{u_1, u_3} F ↥(normalClosure F K L)) (algebraMap F ↥(normalClosure F K L))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K ↥(normalClosure F K L)) (algebraMap F K))

Tactic:
ext x
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra K L
inst_6 : IsScalarTower F K L
x : F
⊢ Eq.{u_3 + 1} (α := L) (↑((algebraMap F ↥(normalClosure F K L) : (a : F) → ↥(normalClosure F K L)) x) : L)
    (↑((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K ↥(normalClosure F K L)) (algebraMap F K) :
            (a : F) → ↥(normalClosure F K L))
          x) :
      L)

Tactic:
algebraMap_apply F K L x

Premises used: IsScalarTower.algebraMap_apply