Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: case e'_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
x✝ : E
⊢ ↑s = Set.range Subtype.val

pp: case e'_3.e'_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
e_1✝ : ↥(adjoin F ↑s) = ↥(adjoin F (Set.range Subtype.val))
⊢ ↑s = Set.range Subtype.val

pp: case e'_5.e'_6
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
e_1✝ : ↥(adjoin F ↑s) = ↥(adjoin F (Set.range Subtype.val))
e_3✝ : (adjoin F ↑s).toField.toCommRing ≍ (adjoin F (Set.range Subtype.val)).toField.toCommRing
⊢ ↑s = Set.range Subtype.val

Tactic:
<;>

Goal state after:
case e'_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
x✝ : E
⊢ ↑s = Set.range Subtype.val

case e'_3.e'_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
e_1✝ : ↥(adjoin F ↑s) = ↥(adjoin F (Set.range Subtype.val))
⊢ ↑s = Set.range Subtype.val

case e'_5.e'_6
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
e_1✝ : ↥(adjoin F ↑s) = ↥(adjoin F (Set.range Subtype.val))
e_3✝ : (adjoin F ↑s).toField.toCommRing ≍ (adjoin F (Set.range Subtype.val)).toField.toCommRing
⊢ ↑s = Set.range Subtype.val