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_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
K : IntermediateField F E
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)

Tactic:
x.2

Premises used: Set.Mem, setOf, IsSeparable, Polynomial.Separable, Subtype.property, 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 : IntermediateField F E
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)

Tactic:
exact x.2

Premises used: 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
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx :
  Membership.mem (γ := IntermediateField F E)
    ((separableClosureOperator F E : (a : IntermediateField F E) → IntermediateField F E)
        (IntermediateField.restrictScalars F (separableClosure K E)) :
      IntermediateField F E)
    x
obtain :
  ∀ (x : ↥(separableClosure K E))
    (hx :
      Membership.mem (α := E) (γ := IntermediateField F E)
        ((separableClosureOperator F E : (a : IntermediateField F E) → IntermediateField F E)
            (IntermediateField.restrictScalars F (separableClosure K E)) :
          IntermediateField F 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 (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 (separableClosure K E)) x

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

Premises used: Eq.le, separableClosure.separableClosure_eq_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 K E
inst_6 : IsScalarTower F K E
x : ↥(separableClosure K E)
hx :
  Membership.mem (α := E) (γ := IntermediateField F E)
    ((separableClosureOperator F E : (a : IntermediateField F E) → IntermediateField F E)
        (IntermediateField.restrictScalars F (separableClosure K E)) :
      IntermediateField F 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 (separableClosure K E))
    ((AlgHom.toRingHom (Algebra.ofId (↥(separableClosure K E)) E) : (a : ↥(separableClosure K E)) → E) x : E)

Tactic:
x.2

Premises used: Set.Mem, setOf, IsSeparable, Polynomial.Separable, Subtype.property, 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 K E
inst_6 : IsScalarTower F K E
x : ↥(separableClosure K E)
hx :
  Membership.mem (α := E) (γ := IntermediateField F E)
    ((separableClosureOperator F E : (a : IntermediateField F E) → IntermediateField F E)
        (IntermediateField.restrictScalars F (separableClosure K E)) :
      IntermediateField F 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 (separableClosure K E))
    ((AlgHom.toRingHom (Algebra.ofId (↥(separableClosure K E)) E) : (a : ↥(separableClosure K E)) → E) x : E)

Tactic:
exact x.2

Premises used: 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
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
L : IntermediateField F E
⊢ LE.le (α := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (separableClosure (↥L) E))
      (IntermediateField.restrictScalars F (separableClosure K E)) ↔
    L ≤ IntermediateField.restrictScalars F (separableClosure K E)

Tactic:
(isClosed_restrictScalars_separableClosure F E K).closure_le_iff

Premises used: Set.Mem, ClosureOperator.IsClosed.closure_le_iff, isClosed_restrictScalars_separableClosure
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ finInsepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (insepDegree F E)

Tactic:
rfl

Premises used: Field.finInsepDegree, Field.insepDegree, Module.finrank, 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
⊢ NeZero (sepDegree F E)

Tactic:
⟨rank_pos.ne'⟩

Premises used: NeZero.mk, LT.lt.ne', rank_pos
-- 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
⊢ NeZero (insepDegree F E)

Tactic:
⟨rank_pos.ne'⟩

Premises used: NeZero.mk, LT.lt.ne', rank_pos
-- 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 : FiniteDimensional F E
⊢ NeZero (finInsepDegree F E)

Tactic:
⟨finrank_pos.ne'⟩

Premises used: NeZero.mk, LT.lt.ne', Module.finrank_pos
-- 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
⊢ Cardinal.lift.{w, v} (sepDegree F E) = Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
i.separableClosure.toLinearEquiv.lift_rank_eq

Premises used: Set.Mem, LinearEquiv.lift_rank_eq, Field.sepDegree, AlgEquiv.separableClosure, AlgEquiv.toLinearEquiv, separableClosure
-- 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 v
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
⊢ sepDegree F E = sepDegree F K

Tactic:
i.separableClosure.toLinearEquiv.rank_eq

Premises used: Set.Mem, Field.sepDegree, AlgEquiv.separableClosure, LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, separableClosure
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ sepDegree F E * insepDegree F E = Module.rank F E

Tactic:
rank_mul_rank F (separableClosure F E) E

Premises used: Set.Mem, rank_mul_rank, Field.sepDegree, Membership.mem, Field.insepDegree, Subtype, separableClosure
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ sepDegree F E ≤ Module.rank F E

Tactic:
Module.rank_bot_le_rank_of_isScalarTower _ _ _

Premises used: Set.Mem, Module.rank_bot_le_rank_of_isScalarTower, Field.sepDegree
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ insepDegree F E ≤ Module.rank F E

Tactic:
Module.rank_top_le_rank_of_isScalarTower _ _ _

Premises used: Module.rank_top_le_rank_of_isScalarTower, Field.insepDegree
-- 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
⊢ Cardinal.lift.{w, v} (insepDegree F E) = Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
Algebra.lift_rank_eq_of_equiv_equiv i.separableClosure i rfl

Premises used: Set.Mem, AlgEquiv.separableClosure, Field.insepDegree, Algebra.lift_rank_eq_of_equiv_equiv, AlgEquiv.toRingEquiv, separableClosure, 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 v
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
⊢ insepDegree F E = insepDegree F K

Tactic:
Algebra.rank_eq_of_equiv_equiv i.separableClosure i rfl

Premises used: Set.Mem, AlgEquiv.separableClosure, Field.insepDegree, Algebra.rank_eq_of_equiv_equiv, AlgEquiv.toRingEquiv, separableClosure, 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
⊢ finInsepDegree F E = finInsepDegree F K

Tactic:
simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat
    (lift_insepDegree_eq_of_equiv F E K i)

Premises used: Cardinal.toNat, Cardinal.toNat_lift, congr_arg, Field.lift_insepDegree_eq_of_equiv, DFunLike.coe
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
inst : Field F
rw : Module.rank F ↥(separableClosure F F) = 1
rw₁ : Module.rank F ↥⊥ = 1
rw₂ rw₃ : Eq.{u + 2} (α := Cardinal.{u}) 1 1
⊢ sepDegree F F = 1

Tactic:
rw [sepDegree, Subsingleton.elim (separableClosure F F) ⊥, IntermediateField.rank_bot]

Premises used: Field.sepDegree, Bot.bot, IntermediateField.rank_bot, Subsingleton.elim, separableClosure
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
inst : Field F
rw : Module.rank (↥(separableClosure F F)) F = 1
rw₁ : Module.rank (↥⊤) F = 1
rw₂ rw₃ : Eq.{u + 2} (α := Cardinal.{u}) 1 1
⊢ insepDegree F F = 1

Tactic:
rw [insepDegree, Subsingleton.elim (separableClosure F F) ⊤, IntermediateField.rank_top]

Premises used: Field.insepDegree, IntermediateField.rank_top, Subsingleton.elim, Top.top, separableClosure
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
inst : Field F
rw : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) (insepDegree F F) : ℕ) (1 : ℕ)
rw₁ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) 1 : ℕ) (1 : ℕ)
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ finInsepDegree F F = 1

Tactic:
rw [finInsepDegree_def', insepDegree_self, Cardinal.one_toNat]

Premises used: Field.insepDegree_self, Field.finInsepDegree_def', Cardinal.one_toNat
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
have :
  ∀ (s : Finset E) (hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤),
    Set.Nonempty.{v} (α := Finset E)
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
⊢ Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}

Tactic:
have ⟨s, hs⟩ := IntermediateField.fg_top F E
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
rw : Algebra.IsIntegral (↥⊤) E
⊢ Algebra.IsAlgebraic (↥(Algebra.adjoin F (↑s : Set E))) E

Tactic:
rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]

Premises used: IntermediateField.isAlgebraic_adjoin_iff_top, Algebra.isAlgebraic_iff_isIntegral
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
⊢ Algebra.IsIntegral (↥⊤) E

Tactic:
Algebra.isIntegral_of_surjective topEquiv.surjective

Premises used: Algebra.isIntegral_of_surjective, AlgEquiv.surjective, IntermediateField.topEquiv
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
⊢ Algebra.IsAlgebraic (↥(Algebra.adjoin F (↑s : Set E))) E

Tactic:
have : Algebra.IsAlgebraic (Algebra.adjoin F (s : Set E)) E := by
      rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]
      refine Algebra.isIntegral_of_surjective topEquiv.surjective
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin F (↑s : Set E))) E
have :
  ∀ (t : Set E) (hts : t ⊆ (↑s : Set E))
    (ht : IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ t }) F (Subtype.val (p := fun (x : E) ↦ x ∈ t))),
    Set.Nonempty.{v} (α := Finset E)
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
⊢ Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}

Tactic:
have ⟨t, hts, ht⟩ := exists_isTranscendenceBasis_subset (R := F) (s : Set E)
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin F (↑s : Set E))) E
t : Set E
hts : t ⊆ (↑s : Set E)
ht : IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ t }) F (Subtype.val (p := fun (x : E) ↦ x ∈ t))
⊢ t.Finite

Tactic:
s.finite_toSet.subset hts

Premises used: Set.Finite.subset, Finset.finite_toSet
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin F (↑s : Set E))) E
t : Set E
hts : t ⊆ (↑s : Set E)
ht : IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ t }) F (Subtype.val (p := fun (x : E) ↦ x ∈ t))
lift :
  ∀ (t : Finset E) (hts : (↑t : Set E) ⊆ (↑s : Set E))
    (ht :
      IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
        (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))),
    Set.Nonempty.{v} (α := Finset E)
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
⊢ Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}

Tactic:
lift t to Finset E using s.finite_toSet.subset hts

Premises used: Finset, Set.Finite.subset, Finset.finite_toSet
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin F (↑s : Set E))) E
t : Finset E
hts : (↑t : Set E) ⊆ (↑s : Set E)
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
⊢ Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}

Tactic:
⟨t, ht⟩

Premises used: Set.Nonempty, Exists.intro
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin F (↑s : Set E))) E
t : Finset E
hts : (↑t : Set E) ⊆ (↑s : Set E)
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
⊢ Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}

Tactic:
exact ⟨t, ht⟩
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
⊢ Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}

Tactic:
have Hexists : {s : Finset E | IsTranscendenceBasis F ((↑) : s → E)}.Nonempty := by
    have ⟨s, hs⟩ := IntermediateField.fg_top F E
    have : Algebra.IsAlgebraic (Algebra.adjoin F (s : Set E)) E := by
      rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]
      refine Algebra.isIntegral_of_surjective topEquiv.surjective
    have ⟨t, hts, ht⟩ := exists_isTranscendenceBasis_subset (R := F) (s : Set E)
    lift t to Finset E using s.finite_toSet.subset hts
    exact ⟨t, ht⟩
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
Hexists :
  Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
s : Finset E :=
  Function.argminOn d
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists
⊢ Membership.mem (γ := Set (Finset E))
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
    (Function.argminOn d
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists)

Tactic:
have hs := d.argminOn_mem _ Hexists
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
Hexists :
  Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
s : Finset E :=
  Function.argminOn d
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists
hs :
  Membership.mem (γ := Set (Finset E))
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
    (Function.argminOn d
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists)
⊢ ∃ (s : Finset E),
    MaximalFor (α := IntermediateField F E)
      (fun (t : Set E) ↦
        IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ t }) F (Subtype.val (p := fun (x : E) ↦ x ∈ t)))
      (fun (t : Set E) ↦ restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E)) (↑s : Set E)

Tactic:
⟨s, hs, fun t ht ↦ not_lt_iff_le_imp_ge.mp fun H ↦ ?_⟩

Premises used: And.intro, Exists.intro, Iff.mp, not_lt_iff_le_imp_ge
-- 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 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
Hexists :
  Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
s : Finset E :=
  Function.argminOn d
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists
hs :
  Membership.mem (γ := Set (Finset E))
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
    (Function.argminOn d
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists)
refine :
  ∀ (t : Set E)
    (ht :
      (fun (t : Set E) ↦
          IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ t }) F (Subtype.val (p := fun (x : E) ↦ x ∈ t)))
        t)
    (H :
      LT.lt.{v} (α := IntermediateField F E)
        ((fun (t : Set E) ↦
            (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
          (↑s : Set E))
        ((fun (t : Set E) ↦
            (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
          t)),
    False
⊢ ∃ (s : Finset E),
    MaximalFor (α := IntermediateField F E)
      (fun (t : Set E) ↦
        IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ t }) F (Subtype.val (p := fun (x : E) ↦ x ∈ t)))
      (fun (t : Set E) ↦ restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E)) (↑s : Set E)

Tactic:
refine ⟨s, hs, fun t ht ↦ not_lt_iff_le_imp_ge.mp fun H ↦ ?_⟩