-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
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))
h :
  ∀ (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))
h₁ :
  ↥(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))
⊢ Algebra.IsAlgebraic (↥(adjoin F (↑s : Set E))) E
have h₂ : ↥(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)))) →
  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: convert! hs.isAlgebraic_field