F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
⊢ f i ≤ ⨆ (i : (i : ι) × { x // x ∈ f i }), adjoin F (rootSet (minpoly F i.snd) E)
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
⊢ ∃ s, x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }) (_ : i ∈ s), adjoin F (rootSet (minpoly F i.snd) E)
refine' exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le (fun i => _)) hx)
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }), adjoin F (rootSet (minpoly F i.snd) E)
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
⊢ f i ≤ ⨆ (i : (i : ι) × { x // x ∈ f i }), adjoin F (rootSet (minpoly F i.snd) E)
intro x1 hx1
case refine'_1
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ adjoin F (rootSet (minpoly F x1) E) ≤
    adjoin F (rootSet (minpoly F { fst := i, snd := { val := x1, property := hx1 } }.snd) E)

case refine'_2
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ rootSet (minpoly F x1) E
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }), adjoin F (rootSet (minpoly F i.snd) E)
refine' SetLike.le_def.mp (le_iSup_of_le ⟨i, x1, hx1⟩ _)
  (subset_adjoin F (rootSet (minpoly F x1) E) _)
no goals
case refine'_1
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ adjoin F (rootSet (minpoly F x1) E) ≤
    adjoin F (rootSet (minpoly F { fst := i, snd := { val := x1, property := hx1 } }.snd) E)
rw [IntermediateField.minpoly_eq, Subtype.coe_mk]
case refine'_2.hp
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ minpoly F x1 ≠ 0
case refine'_2
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ rootSet (minpoly F x1) E
rw [mem_rootSet_of_ne, minpoly.aeval]
no goals
case refine'_2.hp
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F { x // x ∈ f i }
x : E
hx : x ∈ ⨆ (i : ι), f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ minpoly F x1 ≠ 0
exact minpoly.ne_zero (isIntegral_iff.mp (isAlgebraic_iff_isIntegral.mp (h i ⟨x1, hx1⟩)))