-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem exists_finset_of_mem_adjoin {S : Set E} {x : E} (hx : x ∈ adjoin F S) :
    ∃ T : Finset E, (T : Set E) ⊆ S ∧ x ∈ adjoin F (T : Set E)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ adjoin F S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T

Tactic:
simp_rw [← biSup_adjoin_simple S, ← iSup_subtype''] at hx

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ∀ i ∈ s, {↑i} ⊆ ↑(adjoin F (Subtype.val '' ↑s))

Tactic:
rintro _ h _ rfl

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
i✝ : ↑S
h : i✝ ∈ s
⊢ ↑i✝ ∈ ↑(adjoin F (Subtype.val '' ↑s))

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T

Tactic:
refine ⟨s.image Subtype.val, by simp, SetLike.le_def.mp ?_ hx'⟩

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ⨆ i ∈ s, F⟮↑i⟯ ≤ adjoin F ↑(Finset.image Subtype.val s)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ↑(Finset.image Subtype.val s) ⊆ S

Tactic:
simp

Result:
no goals

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T

Tactic:
classical
refine ⟨s.image Subtype.val, by simp, SetLike.le_def.mp ?_ hx'⟩
simp_rw [Finset.coe_image, iSup_le_iff, adjoin_le_iff]
rintro _ h _ rfl
exact subset_adjoin F _ ⟨_, h, rfl⟩

Result:
no goals

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
i✝ : ↑S
h : i✝ ∈ s
⊢ ↑i✝ ∈ ↑(adjoin F (Subtype.val '' ↑s))

Tactic:
exact subset_adjoin F _ ⟨_, h, rfl⟩

Result:
no goals

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ⨆ i ∈ s, F⟮↑i⟯ ≤ adjoin F ↑(Finset.image Subtype.val s)

Tactic:
simp_rw [Finset.coe_image, iSup_le_iff, adjoin_le_iff]

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ∀ i ∈ s, {↑i} ⊆ ↑(adjoin F (Subtype.val '' ↑s))

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T

Tactic:
obtain ⟨s, hx'⟩ := exists_finset_of_mem_iSup hx

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T