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
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)
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)
⊢ t.Finite

Tactic:
simp [Set.Finite, ← Cardinal.mk_lt_aleph0_iff, ht.cardinalMk_eq hs, Cardinal.natCast_lt_aleph0]

Premises used: Set.Finite, IsTranscendenceBasis.cardinalMk_eq, Cardinal.natCast_lt_aleph0, Cardinal.mk_lt_aleph0_iff
-- 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)
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)
⊢ t.Finite

Tactic:
have : t.Finite := by
    simp [Set.Finite, ← Cardinal.mk_lt_aleph0_iff, ht.cardinalMk_eq hs, Cardinal.natCast_lt_aleph0]
-- 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)
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)
this : t.Finite
⊢ t.Finite

Tactic:
this
-- 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)
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)
this : t.Finite
lift :
  ∀ (t : Finset E)
    (ht :
      IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
        (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E))))
    (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 : Set E))),
    False
⊢ False

Tactic:
lift t to Finset E using this

Premises used: Finset
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst_1 : Field F
inst_2 : Field E
inst_3 : Algebra F E
inst_4 : 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)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
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 : Set E))
inst : Algebra.EssFiniteType (↥(adjoin F (↑s : Set E))) E
inst₁ : Algebra.IsAlgebraic (↥(adjoin F (↑s : Set E))) E
⊢ Module.Finite (↥(adjoin F (↑s : Set E))) E

Tactic:
apply +allowSynthFailures Algebra.finite_of_essFiniteType_of_isAlgebraic

Premises used: Algebra.finite_of_essFiniteType_of_isAlgebraic
-- 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)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
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 : Set E))
⊢ Algebra.EssFiniteType (↥(adjoin F (↑s : Set E))) E

Tactic:
.of_comp F _ _

Premises used: Algebra.EssFiniteType.of_comp
-- 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)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
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 : Set E))
⊢ Algebra.EssFiniteType (↥(adjoin F (↑s : Set E))) E

Tactic:
exact .of_comp F _ _
-- 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)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
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 : Set E))
⊢ Algebra.IsAlgebraic
    (↥(adjoin F
        (Set.range (ι :=
          ↥(Function.argminOn d
              {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
              Hexists))
          (Subtype.val (p := fun (x : E) ↦
            x ∈
              Function.argminOn d
                {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
                Hexists)))))
    E

Tactic:
hs.isAlgebraic_field

Premises used: IsTranscendenceBasis.isAlgebraic_field
-- 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)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
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 : Set E))
x : E
⊢ (↑s : Set E) =
    Set.range (ι :=
      ↥(Function.argminOn d
          {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists))
      (Subtype.val (p := fun (x : E) ↦
        x ∈
          Function.argminOn d
            {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
            Hexists))

Tactic:
simp [s]
-- 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)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
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 : Set E))
e_1 :
  ↥(adjoin F (↑s : Set E)) =
    ↥(adjoin F
        (Set.range (ι :=
          ↥(Function.argminOn d
              {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
              Hexists))
          (Subtype.val (p := fun (x : E) ↦
            x ∈
              Function.argminOn d
                {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
                Hexists))))
⊢ (↑s : Set E) =
    Set.range (ι :=
      ↥(Function.argminOn d
          {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists))
      (Subtype.val (p := fun (x : E) ↦
        x ∈
          Function.argminOn d
            {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
            Hexists))

Tactic:
simp [s]
-- 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)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
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 : Set E))
e_1 :
  ↥(adjoin F (↑s : Set E)) =
    ↥(adjoin F
        (Set.range (ι :=
          ↥(Function.argminOn d
              {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
              Hexists))
          (Subtype.val (p := fun (x : E) ↦
            x ∈
              Function.argminOn d
                {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
                Hexists))))
e_3 :
  HEq.{v + 1} (α := CommRing ↥(adjoin F (↑s : Set E))) toCommRing (β :=
    CommRing
      ↥(adjoin F
          (Set.range (ι :=
            ↥(Function.argminOn d
                {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
                Hexists))
            (Subtype.val (p := fun (x : E) ↦
              x ∈
                Function.argminOn d
                  {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
                  Hexists)))))
    toCommRing
⊢ (↑s : Set E) =
    Set.range (ι :=
      ↥(Function.argminOn d
          {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists))
      (Subtype.val (p := fun (x : E) ↦
        x ∈
          Function.argminOn d
            {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
            Hexists))

Tactic:
simp [s]
-- 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)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
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 : Set E))
⊢ Module.Finite (↥(adjoin F (↑s : Set E))) E

Tactic:
have : Module.Finite (adjoin F (s : Set E)) E := by
    apply +allowSynthFailures Algebra.finite_of_essFiniteType_of_isAlgebraic
    · exact .of_comp F _ _
    · convert! hs.isAlgebraic_field <;> simp [s]
-- 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)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
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 : Set E))
this : Module.Finite (↥(adjoin F (↑s : Set E))) E
⊢ Module.Finite (↥(restrictScalars F (L' := ↥(adjoin F (↑s : Set E))) (separableClosure (↥(adjoin F (↑s : Set E))) E)))
    E

Tactic:
have : Module.Finite ((separableClosure (adjoin F (s : Set E)) E).restrictScalars F) E :=
    inferInstanceAs <| Module.Finite (separableClosure (adjoin F (s : Set E)) E) E