-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem sSup_toSubfield (S : Set (IntermediateField F E)) (hS : S.Nonempty) :
    (sSup S).toSubfield = sSup (toSubfield '' S)

Proof state:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
x : IntermediateField F E
a✝ : x ∈ S
⊢ x.toSubfield = Subfield.closure ↑x

Tactic:
exact x.toSubfield.closure_eq.symm

Result:
no goals

Proof state:
case e_s.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
x : F
y : IntermediateField F E
hy : y ∈ S
⊢ (algebraMap F E) x ∈ ⋃₀ (SetLike.coe '' S)

Tactic:
simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]

Result:
case e_s.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
x : F
y : IntermediateField F E
hy : y ∈ S
⊢ ∃ a ∈ S, (algebraMap F E) x ∈ a

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
⊢ Subfield.closure (Set.range ⇑(algebraMap F E) ∪ ⋃₀ (SetLike.coe '' S)) = Subfield.closure (⋃₀ (SetLike.coe '' S))

Tactic:
congr 1

Result:
case e_s
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
⊢ Set.range ⇑(algebraMap F E) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
⊢ (sSup S).toSubfield = sSup (toSubfield '' S)

Tactic:
have h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S) := by
  rw [Set.image_image]
  congr! with x
  exact x.toSubfield.closure_eq.symm

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
⊢ (sSup S).toSubfield = sSup (toSubfield '' S)

Proof state:
case e_s.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
x : F
y : IntermediateField F E
hy : y ∈ S
⊢ ∃ a ∈ S, (algebraMap F E) x ∈ a

Tactic:
exact ⟨y, hy, algebraMap_mem y x⟩

Result:
no goals

Proof state:
case e_s
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
⊢ Set.range ⇑(algebraMap F E) ⊆ ⋃₀ (SetLike.coe '' S)

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case e_s.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
x : F
⊢ (algebraMap F E) x ∈ ⋃₀ (SetLike.coe '' S)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
⊢ (sSup S).toSubfield = sSup (toSubfield '' S)

Tactic:
rw [h, sSup_image, ← Subfield.closure_sUnion, sSup_def, adjoin_toSubfield]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
⊢ Subfield.closure (Set.range ⇑(algebraMap F E) ∪ ⋃₀ (SetLike.coe '' S)) = Subfield.closure (⋃₀ (SetLike.coe '' S))

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
⊢ toSubfield '' S = (fun x => Subfield.closure ↑x) '' S

Tactic:
congr! with x

Result:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
x : IntermediateField F E
a✝ : x ∈ S
⊢ x.toSubfield = Subfield.closure ↑x

Proof state:
case e_s.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
x : F
⊢ (algebraMap F E) x ∈ ⋃₀ (SetLike.coe '' S)

Tactic:
obtain ⟨y, hy⟩ := hS

Result:
case e_s.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
x : F
y : IntermediateField F E
hy : y ∈ S
⊢ (algebraMap F E) x ∈ ⋃₀ (SetLike.coe '' S)

Proof state:
case e_s
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
⊢ Set.range ⇑(algebraMap F E) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)

Tactic:
rw [Set.union_eq_right]

Result:
case e_s
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)
⊢ Set.range ⇑(algebraMap F E) ⊆ ⋃₀ (SetLike.coe '' S)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
⊢ toSubfield '' S = Subfield.closure '' (SetLike.coe '' S)

Tactic:
rw [Set.image_image]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
⊢ toSubfield '' S = (fun x => Subfield.closure ↑x) '' S