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 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:
exact algebraMap_apply F K L x

Premises used: IsScalarTower.algebraMap_apply
-- 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
⊢ IsScalarTower K (↥(normalClosure F K L)) L

Tactic:
of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', 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 K L
inst_6 : IsScalarTower F K L
⊢ Eq (α := IntermediateField F L)
    (IntermediateField.restrictScalars F
      (AlgHom.fieldRange (L := ↥(normalClosure F K L)) (toAlgHom K (↥(normalClosure F K L)) L)))
    (normalClosure F K L)

Tactic:
SetLike.ext' Subtype.range_val

Premises used: Subtype.range_val, SetLike.ext'
-- 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
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
rw : Nonempty (AlgHom.{u_1, u_4, u_3} F (↥(IntermediateField.adjoin F (⨆ (x : K), rootSet (minpoly F x) L'))) L)
⊢ Nonempty (AlgHom.{u_1, u_4, u_3} F (↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L'))) L)

Tactic:
rw [← gc.l_iSup]

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
inst_5 : Algebra.IsAlgebraic F K
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
⊢ Nonempty (AlgHom.{u_1, u_4, u_3} F (↥(IntermediateField.adjoin F (⨆ (x : K), rootSet (minpoly F x) L'))) L)

Tactic:
nonempty_algHom_adjoin_of_splits fun x hx ↦ ?_

Premises used: IntermediateField.nonempty_algHom_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
inst_5 : Algebra.IsAlgebraic F K
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
refine :
  ∀ (x : L') (hx : Membership.mem (γ := Set L') (⨆ (x : K), rootSet (minpoly F x) L') x),
    IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ Nonempty (AlgHom.{u_1, u_4, u_3} F (↥(IntermediateField.adjoin F (⨆ (x : K), rootSet (minpoly F x) L'))) L)

Tactic:
refine nonempty_algHom_adjoin_of_splits fun x hx ↦ ?_

Premises used: IntermediateField.nonempty_algHom_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
inst_5 : Algebra.IsAlgebraic F K
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F 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'), IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ IsIntegral 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
inst_5 : Algebra.IsAlgebraic F K
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F 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'
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))

Tactic:
⟨isAlgebraic_iff_isIntegral.mp (isAlgebraic_of_mem_rootSet hx), ?_⟩

Premises used: And.intro, Iff.mp, isAlgebraic_of_mem_rootSet, 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
inst_5 : Algebra.IsAlgebraic F K
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F 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'
refine : Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))

Tactic:
refine ⟨isAlgebraic_iff_isIntegral.mp (isAlgebraic_of_mem_rootSet hx), ?_⟩
-- 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
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F 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
inst_5 : Algebra.IsAlgebraic F K
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F 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:
(h 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
inst_5 : Algebra.IsAlgebraic F K
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F 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 (h 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
inst_5 : Algebra.IsAlgebraic F K
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F 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
inst_5 : Algebra.IsAlgebraic F K
h_1 : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
φ : AlgHom.{u_1, u_4, u_3} F (↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L'))) L := Nonempty.some ⋯
φ' : AlgHom.{u_1, u_4, u_3} F (↥(normalClosure F K L')) L := φ.comp (inclusion ⋯)
x x_1 : K →ₐ[F] L'
h :
  Eq (α := K →ₐ[F] L)
    ((φ'.comp ∘ (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
      x)
    ((φ'.comp ∘ (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
      x_1)
rw :
  ∀
    (h :
      Eq (α := (a : K) → L)
        (⇑((φ'.comp ∘
                (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
              x) :
          (a : K) → L)
        (⇑((φ'.comp ∘
                (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
              x_1) :
          (a : K) → L)),
    Eq (α := (a : K) → ↥(normalClosure F K L'))
      (⇑((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x :
            AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L')) :
        (a : K) → ↥(normalClosure F K L'))
      (⇑((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x_1 :
            AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L')) :
        (a : K) → ↥(normalClosure F K L'))
⊢ Eq (α := AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L'))
    ((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x :
      AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L'))
    ((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x_1 :
      AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L'))

Tactic:
rw [DFunLike.ext'_iff] at h ⊢

Premises used: DFunLike.ext'_iff
-- 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
h_1 : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
φ : AlgHom.{u_1, u_4, u_3} F (↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L'))) L := Nonempty.some ⋯
φ' : AlgHom.{u_1, u_4, u_3} F (↥(normalClosure F K L')) L := φ.comp (inclusion ⋯)
x x_1 : K →ₐ[F] L'
h :
  Eq (α := (a : K) → L)
    (⇑((φ'.comp ∘
            (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
          x) :
      (a : K) → L)
    (⇑((φ'.comp ∘
            (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
          x_1) :
      (a : K) → L)
⊢ Eq (α := (a : K) → ↥(normalClosure F K L'))
    (⇑((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x :
          AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L')) :
      (a : K) → ↥(normalClosure F K L'))
    (⇑((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x_1 :
          AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L')) :
      (a : K) → ↥(normalClosure F K L'))

Tactic:
φ'.injective.comp_left h

Premises used: RingHom.injective, AlgHom.toRingHom, Function.Injective.comp_left
-- 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
h_1 : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
φ : AlgHom.{u_1, u_4, u_3} F (↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L'))) L := Nonempty.some ⋯
φ' : AlgHom.{u_1, u_4, u_3} F (↥(normalClosure F K L')) L := φ.comp (inclusion ⋯)
x x_1 : K →ₐ[F] L'
h :
  Eq (α := (a : K) → L)
    (⇑((φ'.comp ∘
            (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
          x) :
      (a : K) → L)
    (⇑((φ'.comp ∘
            (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
          x_1) :
      (a : K) → L)
⊢ Eq (α := (a : K) → ↥(normalClosure F K L'))
    (⇑((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x :
          AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L')) :
      (a : K) → ↥(normalClosure F K L'))
    (⇑((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x_1 :
          AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L')) :
      (a : K) → ↥(normalClosure F K L'))

Tactic:
exact φ'.injective.comp_left h

Premises used: RingHom.injective, AlgHom.toRingHom, Function.Injective.comp_left
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
⊢ K ≤ normalClosure F (↥K) L

Tactic:
K.fieldRange_val.symm.trans_le K.val.fieldRange_le_normalClosure

Premises used: Eq.trans_le, AlgHom.fieldRange_le_normalClosure, IntermediateField.val, IntermediateField.fieldRange_val, Eq.symm
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal.{u_1, u_3} F ↥K
⊢ normalClosure F (↥K) L = K

Tactic:
simp only [normalClosure_def, AlgHom.fieldRange_of_normal, iSup_const]

Premises used: normalClosure_def, iSup_const, AlgHom.fieldRange_of_normal
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥K) L) (⨆ (f : L →ₐ[F] L), map f K)

Tactic:
(normalClosure_def F K L).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))

Premises used: Membership.mem, Subtype, normalClosure_def, le_antisymm, iSup_le, Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
refine_1 : ∀ (f : ↥K →ₐ[F] L), f.fieldRange ≤ ⨆ (f : L →ₐ[F] L), map f K
refine_2 : ∀ (f : L →ₐ[F] L), map f K ≤ ⨆ (f : ↥K →ₐ[F] L), f.fieldRange
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥K) L) (⨆ (f : L →ₐ[F] L), map f K)

Tactic:
refine (normalClosure_def F K L).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))

Premises used: Membership.mem, Subtype, normalClosure_def, le_antisymm, iSup_le, Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
f : ↥K →ₐ[F] L
⊢ f.fieldRange ≤ ⨆ (f : L →ₐ[F] L), map f K

Tactic:
le_iSup_of_le (f.liftNormal L) (fun b ⟨a, h⟩ ↦ ⟨a, a.2, h ▸ f.liftNormal_commutes L a⟩)

Premises used: _private.0.IntermediateField.normalClosure_def'.match_1, Set.Mem, Membership.mem, AlgHom.liftNormal, Eq.rec, AlgHom.liftNormal_commutes, le_iSup_of_le, And.intro, Exists.intro, Subtype.val, IntermediateField.map, Subtype.property
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
f : ↥K →ₐ[F] L
⊢ f.fieldRange ≤ ⨆ (f : L →ₐ[F] L), map f K

Tactic:
exact le_iSup_of_le (f.liftNormal L) (fun b ⟨a, h⟩ ↦ ⟨a, a.2, h ▸ f.liftNormal_commutes L a⟩)

Premises used: AlgHom.liftNormal, le_iSup_of_le
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ (f : ↥K →ₐ[F] L), f.fieldRange

Tactic:
le_iSup_of_le (f.comp K.val) (fun b ⟨a, h⟩ ↦ ⟨⟨a, h.1⟩, h.2⟩)

Premises used: Set.Mem, Membership.mem, Subtype.mk, AlgHom.fieldRange, And.right, And.left, le_iSup_of_le, Exists.intro, IntermediateField.val, _private.0.IntermediateField.normalClosure_def'.match_2, AlgHom.comp
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ (f : ↥K →ₐ[F] L), f.fieldRange

Tactic:
exact le_iSup_of_le (f.comp K.val) (fun b ⟨a, h⟩ ↦ ⟨⟨a, h.1⟩, h.2⟩)

Premises used: le_iSup_of_le, IntermediateField.val, AlgHom.comp
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥K) L) (⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K)

Tactic:
(normalClosure_def' K).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))

Premises used: le_antisymm, iSup_le, IntermediateField.normalClosure_def', Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
refine_1 : ∀ (f : L →ₐ[F] L), map f K ≤ ⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K
refine_2 : ∀ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K ≤ ⨆ (f : L →ₐ[F] L), map f K
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥K) L) (⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K)

Tactic:
refine (normalClosure_def' K).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))

Premises used: le_antisymm, iSup_le, IntermediateField.normalClosure_def', Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K

Tactic:
le_iSup_of_le (f.restrictNormal' L)
      (fun b ⟨a, h⟩ ↦ ⟨a, h.1, h.2 ▸ f.restrictNormal_commutes L a⟩)

Premises used: AlgEquiv.toAlgHom, Set.Mem, Membership.mem, Eq.rec, And.right, And.left, le_iSup_of_le, And.intro, Exists.intro, AlgHom.restrictNormal', _private.0.IntermediateField.normalClosure_def'.match_2, AlgHom.restrictNormal_commutes, IntermediateField.map
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K

Tactic:
exact le_iSup_of_le (f.restrictNormal' L)
      (fun b ⟨a, h⟩ ↦ ⟨a, h.1, h.2 ▸ f.restrictNormal_commutes L a⟩)

Premises used: le_iSup_of_le, AlgHom.restrictNormal'
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
f : Gal(L/F)
⊢ map (↑f : L →ₐ[F] L) K ≤ ⨆ (f : L →ₐ[F] L), map f K

Tactic:
exact le_iSup_of_le f le_rfl

Premises used: le_rfl, le_iSup_of_le
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K K' : IntermediateField F L
inst_3 : Normal F L
h : K ≤ K'
rw : LE.le.{u_3} (α := IntermediateField F L) (⨆ (f : L →ₐ[F] L), map f K) (⨆ (f : L →ₐ[F] L), map f K')
⊢ LE.le (α := IntermediateField F L) (normalClosure F (↥K) L) (normalClosure F (↥K') L)

Tactic:
rw [normalClosure_def', normalClosure_def']

Premises used: IntermediateField.normalClosure_def'
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K K' : IntermediateField F L
inst_3 : Normal F L
h : K ≤ K'
⊢ LE.le.{u_3} (α := IntermediateField F L) (⨆ (f : L →ₐ[F] L), map f K) (⨆ (f : L →ₐ[F] L), map f K')

Tactic:
iSup_mono (fun f ↦ map_mono f h)

Premises used: IntermediateField.map_mono, Set.Mem, iSup_mono
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K K' : IntermediateField F L
inst_3 : Normal F L
h : K ≤ K'
⊢ LE.le.{u_3} (α := IntermediateField F L) (⨆ (f : L →ₐ[F] L), map f K) (⨆ (f : L →ₐ[F] L), map f K')

Tactic:
exact iSup_mono (fun f ↦ map_mono f h)

Premises used: IntermediateField.map_mono, iSup_mono
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
⊢ Normal.{u_1, u_3} F ↥K ↔ normalClosure F (↥K) L = K

Tactic:
⟨@normalClosure_of_normal (K := K), fun h ↦ h ▸ normalClosure.normal F K L⟩

Premises used: Membership.mem, Eq.rec, Subtype, IntermediateField.normalClosure_of_normal, Iff.intro, normalClosure.normal
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
⊢ Normal.{u_1, u_3} F ↥K ↔ normalClosure F (↥K) L ≤ K

Tactic:
normal_iff_normalClosure_eq.trans (le_normalClosure K).ge_iff_eq'.symm

Premises used: LE.le.ge_iff_eq', Iff.trans, IntermediateField.le_normalClosure, Iff.symm, IntermediateField.normal_iff_normalClosure_eq
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
rw₁ : ⨆ (f : ↥K →ₐ[F] L), f.fieldRange ≤ K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
rw₂ rw₃ : (∀ (i : ↥K →ₐ[F] L), i.fieldRange ≤ K) ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K

Tactic:
rw [normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff]

Premises used: IntermediateField.normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
rw₁ : ⨆ (f : L →ₐ[F] L), map f K ≤ K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
rw₂ rw₃ : (∀ (i : L →ₐ[F] L), map i K ≤ K) ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K

Tactic:
rw [normal_iff_normalClosure_le, normalClosure_def', iSup_le_iff]

Premises used: IntermediateField.normal_iff_normalClosure_le, iSup_le_iff, IntermediateField.normalClosure_def'
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
rw₁ : ⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K ≤ K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
rw₂ rw₃ : (∀ (i : Gal(L/F)), map (↑i : L →ₐ[F] L) K ≤ K) ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K

Tactic:
rw [normal_iff_normalClosure_le, normalClosure_def'', iSup_le_iff]

Premises used: IntermediateField.normal_iff_normalClosure_le, IntermediateField.normalClosure_def'', iSup_le_iff