awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (separableClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (separableClosure F E) x

Tactic:
map_mem_separableClosure_iff i

Premises used: Set.Mem, setOf, map_mem_separableClosure_iff, Set.preimage, IsSeparable, Polynomial.Separable, IsCoprime
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (separableClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (separableClosure F E) x

Tactic:
exact map_mem_separableClosure_iff i

Premises used: map_mem_separableClosure_iff
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
⊢ IntermediateField.map i (separableClosure F E) ≤ separableClosure F K

Tactic:
map_le_iff_le_comap.2 (comap_eq_of_algHom i).ge

Premises used: Iff.mpr, IntermediateField.map_le_iff_le_comap, Eq.ge, separableClosure.comap_eq_of_algHom
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : Eq (α := IntermediateField E K) (separableClosure E K) ⊥
⊢ Eq (α := IntermediateField F K) (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E))
    (separableClosure F K)

Tactic:
le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)

Premises used: separableClosure.map_le_of_algHom, le_antisymm
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : Eq (α := IntermediateField E K) (separableClosure E K) ⊥
refine :
  ∀ (x : K) (hx : Membership.mem (γ := IntermediateField F K) (separableClosure F K) x),
    Membership.mem (γ := IntermediateField F K)
      (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)) x
⊢ Eq (α := IntermediateField F K) (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E))
    (separableClosure F K)

Tactic:
refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)

Premises used: separableClosure.map_le_of_algHom, le_antisymm
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : Eq (α := IntermediateField E K) (separableClosure E K) ⊥
x : K
hx : Membership.mem (γ := IntermediateField F K) (separableClosure F K) x
obtain :
  ∀ (y : E)
    (hx :
      Membership.mem (α := K) (γ := IntermediateField F K) (separableClosure F K)
        ((algebraMap E K : (a : E) → K) y : K)),
    Membership.mem (α := K) (γ := IntermediateField F K)
      (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E))
      ((algebraMap E K : (a : E) → K) y : K)
⊢ Membership.mem (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)) x

Tactic:
obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_separableClosure_iff.2
    (IsSeparable.tower_top E <| mem_separableClosure_iff.1 hx)

Premises used: Iff.mp, IntermediateField.mem_bot, rfl
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : Eq (α := IntermediateField E K) (separableClosure E K) ⊥
y : E
hx : Membership.mem (α := K) (γ := IntermediateField F K) (separableClosure F K) ((algebraMap E K : (a : E) → K) y : K)
⊢ Membership.mem (α := K) (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)) ((algebraMap E K : (a : E) → K) y : K)

Tactic:
⟨y, (map_mem_separableClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩

Premises used: Set.Mem, setOf, IsScalarTower.toAlgHom, map_mem_separableClosure_iff, And.intro, Exists.intro, Iff.mp, Set.image, rfl
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x : K
h : Membership.mem (γ := IntermediateField F K) (separableClosure F K) x
⊢ ((↑(↑i : E →ₐ[F] K) : E →+* K) : (a : E) → K) (((↑i.symm : K →ₐ[F] E) : (a : K) → E) x : E) = x

Tactic:
simp
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
⊢ Algebra.IsAlgebraic.{u, v} F ↥(separableClosure F E)

Tactic:
⟨fun x ↦ isAlgebraic_iff.2 (IsSeparable.isIntegral x.2).isAlgebraic⟩

Premises used: Iff.mpr, IntermediateField.isAlgebraic_iff, IsIntegral.isAlgebraic, Algebra.IsAlgebraic.mk, Subtype.property, IsSeparable.isIntegral
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
x : ↥(separableClosure F E)
⊢ IsSeparable F x

Tactic:
simpa only [IsSeparable, minpoly_eq] using x.2

Premises used: IntermediateField.minpoly_eq, IsSeparable, Subtype.property
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
hs : ∀ (x : ↥L), IsSeparable F x
x : E
h : x ∈ L
⊢ Membership.mem (γ := IntermediateField F E) (separableClosure F E) x

Tactic:
simpa only [IsSeparable, minpoly_eq] using hs ⟨x, h⟩

Premises used: Subtype.mk, IntermediateField.minpoly_eq, IsSeparable
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
inst_3 : Algebra.IsSeparable.{u, v} F ↥L
⊢ L ≤ separableClosure F E

Tactic:
le_separableClosure' F E (Algebra.IsSeparable.isSeparable F)

Premises used: Algebra.IsSeparable.isSeparable, le_separableClosure'
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
⊢ L ≤ separableClosure F E ↔ Algebra.IsSeparable.{u, v} F ↥L

Tactic:
Subalgebra.isSeparable_iff.symm

Premises used: Set.Mem, setOf, Subalgebra.isSeparable_iff, IsSeparable, Polynomial.Separable, Iff.symm, IsCoprime
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := IntermediateField (↥(separableClosure F E)) E) (separableClosure (↥(separableClosure F E)) E) ⊥

Tactic:
bot_unique fun x hx ↦ mem_bot.2
    ⟨⟨x, IsSeparable.of_algebra_isSeparable_of_isSeparable F (mem_separableClosure_iff.1 hx)⟩, rfl⟩

Premises used: Iff.mpr, IsSeparable.of_algebra_isSeparable_of_isSeparable, Subtype.mk, Exists.intro, Iff.mp, bot_unique, mem_separableClosure_iff, IntermediateField.mem_bot, rfl
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := IntermediateField F E) (normalClosure F (↥(separableClosure F E)) E) (separableClosure F E)

Tactic:
le_antisymm (normalClosure_le_iff.2 fun i ↦
    have : Algebra.IsSeparable F i.fieldRange :=
      (AlgEquiv.Algebra.isSeparable (AlgEquiv.ofInjectiveField i))
    le_separableClosure F E _) (le_normalClosure _)

Premises used: normalClosure_le_iff, Iff.mpr, AlgEquiv.ofInjectiveField, AlgHom.fieldRange, le_antisymm, AlgEquiv.Algebra.isSeparable, le_separableClosure, IntermediateField.le_normalClosure
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Normal F E
rw : Normal.{u, v} F ↥(normalClosure F (↥(separableClosure F E)) E)
⊢ Normal.{u, v} F ↥(separableClosure F E)

Tactic:
rw [← separableClosure.normalClosure_eq_self]

Premises used: separableClosure.normalClosure_eq_self
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Normal F E
⊢ Normal.{u, v} F ↥(normalClosure F (↥(separableClosure F E)) E)

Tactic:
normalClosure.normal F _ E

Premises used: normalClosure.normal
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Normal F E
⊢ Normal.{u, v} F ↥(normalClosure F (↥(separableClosure F E)) E)

Tactic:
exact normalClosure.normal F _ E

Premises used: normalClosure.normal
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsSepClosed E
⊢ Eq (α := IntermediateField F E) (separableClosure F E) ⊥ ↔ IsSepClosed F

Tactic:
⟨fun h ↦ IsSepClosed.of_exists_root _ fun p _ hirr hsep ↦ ?_,
    fun _ ↦ IntermediateField.eq_bot_of_isSepClosed_of_isSeparable _⟩

Premises used: IsSepClosed.of_exists_root, Iff.intro, IntermediateField.eq_bot_of_isSepClosed_of_isSeparable, separableClosure
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsSepClosed E
refine :
  ∀ (h : Eq (α := IntermediateField F E) (separableClosure F E) ⊥) (p : F[X]),
    p.Monic → ∀ (hirr : Irreducible p) (hsep : p.Separable), ∃ (x : F), eval x p = 0
⊢ Eq (α := IntermediateField F E) (separableClosure F E) ⊥ ↔ IsSepClosed F

Tactic:
refine ⟨fun h ↦ IsSepClosed.of_exists_root _ fun p _ hirr hsep ↦ ?_,
    fun _ ↦ IntermediateField.eq_bot_of_isSepClosed_of_isSeparable _⟩
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsSepClosed E
h : Eq (α := IntermediateField F E) (separableClosure F E) ⊥
p : F[X]
h_1 : p.Monic
hirr : Irreducible p
hsep : p.Separable
obtain : ∀ (x : E) (hx : Eq.{v + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)), ∃ (x : F), eval x p = 0
⊢ ∃ (x : F), eval x p = 0

Tactic:
obtain ⟨x, hx⟩ := IsSepClosed.exists_aeval_eq_zero E p (degree_pos_of_irreducible hirr).ne' hsep

Premises used: LT.lt.ne', Polynomial.degree_pos_of_irreducible, IsSepClosed.exists_aeval_eq_zero
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsSepClosed E
h : Eq (α := IntermediateField F E) (separableClosure F E) ⊥
p : F[X]
h_1 : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : E
hx : Eq.{v + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)
obtain :
  ∀ (x : F)
    (hx :
      Eq.{v + 1} (α := E)
        (((aeval ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) x) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E)
        (0 : E)),
    ∃ (x : F), eval x p = 0
⊢ ∃ (x : F), eval x p = 0

Tactic:
obtain ⟨x, rfl⟩ := h ▸ mem_separableClosure_iff.2 (hsep.of_dvd <| minpoly.dvd _ x hx)

Premises used: rfl
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsSepClosed E
h : Eq (α := IntermediateField F E) (separableClosure F E) ⊥
p : F[X]
h_1 : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : F
hx :
  Eq.{v + 1} (α := E)
    (((aeval ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) x) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E) (0 : E)
⊢ eval x p = 0

Tactic:
simpa [Algebra.ofId_apply] using hx

Premises used: Algebra.ofId_apply
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsSepClosed E
h : Eq (α := IntermediateField F E) (separableClosure F E) ⊥
p : F[X]
h_1 : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : F
hx :
  Eq.{v + 1} (α := E)
    (((aeval ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) x) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E) (0 : E)
⊢ ∃ (x : F), eval x p = 0

Tactic:
exact ⟨x, by simpa [Algebra.ofId_apply] using hx⟩
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : IsSepClosed E
⊢ IsSepClosure.{u, v} F ↥(separableClosure F E)

Tactic:
⟨(IsSepClosed.separableClosure_eq_bot_iff _ E).mp (separableClosure.separableClosure_eq_bot F E),
    isSeparable F E⟩

Premises used: IsSepClosure.mk, Iff.mp, separableClosure.isSeparable, IsSepClosed.separableClosure_eq_bot_iff, separableClosure.separableClosure_eq_bot
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
⊢ IsSepClosed.{u} (SeparableClosure F)

Tactic:
(inferInstance : IsSepClosure F (SeparableClosure F)).sep_closed

Premises used: IsSepClosure.sep_closed
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ Algebra.IsSeparable.{u, v} F ↥(adjoin F S) ↔ ∀ x ∈ S, IsSeparable F x

Tactic:
(le_separableClosure_iff F E _).symm.trans adjoin_le_iff

Premises used: IntermediateField.adjoin_le_iff, le_separableClosure_iff, Iff.trans, Iff.symm
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := IntermediateField F E) (separableClosure F E) ⊤ ↔ Algebra.IsSeparable F E

Tactic:
⟨fun h ↦ ⟨fun _ ↦ mem_separableClosure_iff.1 (h ▸ mem_top)⟩,
    fun _ ↦ top_unique fun x _ ↦ mem_separableClosure_iff.2 (Algebra.IsSeparable.isSeparable _ x)⟩

Premises used: Iff.mpr, Algebra.IsSeparable.isSeparable, IntermediateField.mem_top, Eq.rec, top_unique, Iff.intro, Iff.mp, mem_separableClosure_iff, Eq.symm, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ LE.le (α := IntermediateField F K) (separableClosure F K) (IntermediateField.restrictScalars F (separableClosure E K))

Tactic:
fun _ ↦ IsSeparable.tower_top E

Premises used: Set.Mem, setOf, IsSeparable.tower_top, IsSeparable, Polynomial.Separable, IsCoprime
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
⊢ Eq (α := IntermediateField F K) (separableClosure F K) (IntermediateField.restrictScalars F (separableClosure E K))

Tactic:
(separableClosure.le_restrictScalars F E K).antisymm fun _ h ↦
    IsSeparable.of_algebra_isSeparable_of_isSeparable F h

Premises used: IsSeparable.of_algebra_isSeparable_of_isSeparable, LE.le.antisymm, separableClosure.le_restrictScalars
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ LE.le (α := IntermediateField E K) (adjoin E (↑(separableClosure F K) : Set K)) (separableClosure E K)

Tactic:
adjoin_le_iff.2 <| le_restrictScalars F E K

Premises used: Iff.mpr, IntermediateField.adjoin_le_iff, separableClosure.le_restrictScalars
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
L1 L2 : IntermediateField F E
h1 : Algebra.IsSeparable.{u, v} F ↥L1
h2 : Algebra.IsSeparable.{u, v} F ↥L2
rw : ∀ (h1 : L1 ≤ separableClosure F E) (h2 : L2 ≤ separableClosure F E), L1 ⊔ L2 ≤ separableClosure F E
⊢ Algebra.IsSeparable.{u, v} F ↥(L1 ⊔ L2)

Tactic:
rw [← le_separableClosure_iff] at h1 h2 ⊢

Premises used: le_separableClosure_iff
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
L1 L2 : IntermediateField F E
h1 : L1 ≤ separableClosure F E
h2 : L2 ≤ separableClosure F E
⊢ L1 ⊔ L2 ≤ separableClosure F E

Tactic:
sup_le h1 h2

Premises used: sup_le
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
L1 L2 : IntermediateField F E
h1 : L1 ≤ separableClosure F E
h2 : L2 ≤ separableClosure F E
⊢ L1 ⊔ L2 ≤ separableClosure F E

Tactic:
exact sup_le h1 h2

Premises used: sup_le
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
ι : Type u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsSeparable.{u, v} F ↥(t i)
simp_rw :
  ∀ (h : ∀ (i : ι), t i ≤ separableClosure F E),
    LE.le (α := IntermediateField F E) (⨆ (i : ι), t i) (separableClosure F E)
⊢ Algebra.IsSeparable.{u, v} F ↥(⨆ (i : ι), t i)

Tactic:
simp_rw [← le_separableClosure_iff] at h ⊢

Premises used: le_separableClosure_iff
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
ι : Type u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), t i ≤ separableClosure F E
⊢ LE.le (α := IntermediateField F E) (⨆ (i : ι), t i) (separableClosure F E)

Tactic:
iSup_le h

Premises used: Set.Mem, iSup_le
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
ι : Type u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), t i ≤ separableClosure F E
⊢ LE.le (α := IntermediateField F E) (⨆ (i : ι), t i) (separableClosure F E)

Tactic:
exact iSup_le h

Premises used: iSup_le
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
⊢ L ≤ IntermediateField.restrictScalars F (L' := ↥L) (separableClosure (↥L) E)

Tactic:
fun x hx ↦ isSeparable_algebraMap (F := L) ⟨x, hx⟩

Premises used: Set.Mem, isSeparable_algebraMap, setOf, Subtype.mk, IsSeparable, Polynomial.Separable, IsCoprime
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
refine_1 :
  ∀ (K L : IntermediateField F E) (le : K ≤ L) (x : E)
    (hx :
      Membership.mem (γ := IntermediateField F E)
        ((fun (K : IntermediateField F E) ↦
            (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
          K)
        x),
    Membership.mem (γ := IntermediateField F E)
      ((fun (K : IntermediateField F E) ↦
          (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
        L)
      x
refine_2 :
  ∀ (K : IntermediateField F E) (x : E)
    (hx :
      Membership.mem (γ := IntermediateField F E)
        ((fun (K : IntermediateField F E) ↦
            (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
          ((fun (K : IntermediateField F E) ↦
              (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
            K))
        x),
    Membership.mem (γ := IntermediateField F E)
      ((fun (K : IntermediateField F E) ↦
          (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
        K)
      x
⊢ ClosureOperator (IntermediateField F E)

Tactic:
refine .mk' (fun K ↦ (separableClosure K E).restrictScalars F) (fun K L le x hx ↦ ?_)
    le_restrictScalars_separableClosure fun K x hx ↦ ?_
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
K L : IntermediateField F E
le : K ≤ L
x : E
hx :
  Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E))
    x
x_1 : Algebra ↥K ↥L := (inclusion le).toAlgebra
⊢ IsScalarTower (↥K) (↥L) E

Tactic:
have : IsScalarTower K L E := .of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
K L : IntermediateField F E
le : K ≤ L
x : E
hx :
  Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E))
    x
x_1 : Algebra ↥K ↥L := (inclusion le).toAlgebra
this : IsScalarTower (↥K) (↥L) E
⊢ Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (separableClosure (↥L) E))
    x

Tactic:
hx.tower_top _

Premises used: Set.Mem, setOf, IsSeparable.tower_top, IsSeparable, Polynomial.Separable, IsCoprime
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
K L : IntermediateField F E
le : K ≤ L
x : E
hx :
  Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E))
    x
x_1 : Algebra ↥K ↥L := (inclusion le).toAlgebra
this : IsScalarTower (↥K) (↥L) E
⊢ Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (separableClosure (↥L) E))
    x

Tactic:
exact hx.tower_top _

Premises used: IsSeparable.tower_top
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
K : IntermediateField F E
x : E
hx :
  Membership.mem (γ := IntermediateField F E)
    (IntermediateField.restrictScalars F (L' :=
      ↥(IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E)))
      (separableClosure (↥(IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E))) E))
    x
refine_2 :
  ∀ (x : ↥(separableClosure (↥K) E))
    (hx :
      Membership.mem (α := E) (γ := IntermediateField F E)
        (IntermediateField.restrictScalars F (L' :=
          ↥(IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E)))
          (separableClosure (↥(IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E))) E))
        ((AlgHom.toRingHom (Algebra.ofId (↥(separableClosure (↥K) E)) E) : (a : ↥(separableClosure (↥K) E)) → E) x :
          E)),
    Membership.mem (α := E) (γ := IntermediateField F E)
      (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E))
      ((AlgHom.toRingHom (Algebra.ofId (↥(separableClosure (↥K) E)) E) : (a : ↥(separableClosure (↥K) E)) → E) x : E)
⊢ Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E))
    x

Tactic:
obtain ⟨x, rfl⟩ := (separableClosure.separableClosure_eq_bot K E).le hx

Premises used: Membership.mem, Subtype, Eq.le, separableClosure.separableClosure_eq_bot, rfl