F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ ↑(restrictScalars F (adjoin { x // x ∈ adjoin F S } T)) = ↑(adjoin F (S ∪ T))
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ restrictScalars F (adjoin { x // x ∈ adjoin F S } T) = adjoin F (S ∪ T)
rw [SetLike.ext'_iff]
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ ↑(adjoin { x // x ∈ adjoin F S } T) = ↑(adjoin F (S ∪ T))
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ ↑(restrictScalars F (adjoin { x // x ∈ adjoin F S } T)) = ↑(adjoin F (S ∪ T))
change (↑(adjoin (adjoin F S) T) : Set E) = _
case a.left
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E) ⊆ ↑(adjoin F (S ∪ T))

case a.right
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ T ⊆ ↑(adjoin F (S ∪ T))

case a.left
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ↑(algebraMap F E) ⊆ ↑(adjoin { x // x ∈ adjoin F S } T)

case a.right
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin { x // x ∈ adjoin F S } T)
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ ↑(adjoin { x // x ∈ adjoin F S } T) = ↑(adjoin F (S ∪ T))
apply Set.eq_of_subset_of_subset <;> rw [adjoin_subset_adjoin_iff] <;> constructor
case a.left.intro.mk
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ adjoin F S
⊢ ↑(algebraMap { x // x ∈ adjoin F S } E) { val := x, property := hx } ∈ ↑(adjoin F (S ∪ T))
case a.left
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E) ⊆ ↑(adjoin F (S ∪ T))
rintro _ ⟨⟨x, hx⟩, rfl⟩
no goals
case a.left.intro.mk
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ adjoin F S
⊢ ↑(algebraMap { x // x ∈ adjoin F S } E) { val := x, property := hx } ∈ ↑(adjoin F (S ∪ T))
exact adjoin.mono _ _ _ (Set.subset_union_left _ _) hx
no goals
case a.right
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ T ⊆ ↑(adjoin F (S ∪ T))
exact subset_adjoin_of_subset_right _ _ (Set.subset_union_right _ _)
case a.left.intro
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
f : F
⊢ ↑(algebraMap F E) f ∈ ↑(adjoin { x // x ∈ adjoin F S } T)
case a.left
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ↑(algebraMap F E) ⊆ ↑(adjoin { x // x ∈ adjoin F S } T)
rintro x ⟨f, rfl⟩
case a.left.intro
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
f : F
⊢ ↑(algebraMap F E) f ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E) ∪ T
case a.left.intro
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
f : F
⊢ ↑(algebraMap F E) f ∈ ↑(adjoin { x // x ∈ adjoin F S } T)
refine' Subfield.subset_closure _
case a.left.intro.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
f : F
⊢ ↑(algebraMap F E) f ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E)
case a.left.intro
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
f : F
⊢ ↑(algebraMap F E) f ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E) ∪ T
left
no goals
case a.left.intro.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
f : F
⊢ ↑(algebraMap F E) f ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E)
exact ⟨f, rfl⟩
case a.right.refine'_1
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ S
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E) ∪ T

case a.right.refine'_2
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ T
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E) ∪ T
case a.right
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin { x // x ∈ adjoin F S } T)
refine' Set.union_subset (fun x hx => Subfield.subset_closure _)
  (fun x hx => Subfield.subset_closure _)
case a.right.refine'_1.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ S
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E)
case a.right.refine'_1
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ S
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E) ∪ T
left
case a.right.refine'_1.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ S
⊢ x ∈ Set.range ↑(algebraMap F E) ∪ S
case a.right.refine'_1.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ S
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E)
refine' ⟨⟨x, Subfield.subset_closure _⟩, rfl⟩
case a.right.refine'_1.h.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ S
⊢ x ∈ S
case a.right.refine'_1.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ S
⊢ x ∈ Set.range ↑(algebraMap F E) ∪ S
right
no goals
case a.right.refine'_1.h.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ S
⊢ x ∈ S
exact hx
case a.right.refine'_2.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ T
⊢ x ∈ T
case a.right.refine'_2
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ T
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ adjoin F S } E) ∪ T
right
no goals
case a.right.refine'_2.h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
x : E
hx : x ∈ T
⊢ x ∈ T
exact hx