case h
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
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E'
⊢ x ∈ map f (adjoin F S) ↔ x ∈ adjoin F (↑f '' S)
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
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E →ₐ[F] E'
⊢ map f (adjoin F S) = adjoin F (↑f '' S)
ext x
case h
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
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E'
⊢ x ∈ Subfield.map (↑f) (Subfield.closure (Set.range ↑(algebraMap F E) ∪ S)) ↔
    x ∈ Subfield.closure (Set.range ↑(algebraMap F E') ∪ ↑f '' S)
case h
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
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E'
⊢ x ∈ map f (adjoin F S) ↔ x ∈ adjoin F (↑f '' S)
show
  x ∈ (Subfield.closure (Set.range (algebraMap F E) ∪ S)).map (f : E →+* E') ↔
    x ∈ Subfield.closure (Set.range (algebraMap F E') ∪ f '' S)
case h
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
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E'
⊢ x ∈ Subfield.closure (Set.range ↑(algebraMap F E') ∪ ↑↑f '' S) ↔
    x ∈ Subfield.closure (Set.range ↑(algebraMap F E') ∪ ↑f '' S)
case h
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
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E'
⊢ x ∈ Subfield.map (↑f) (Subfield.closure (Set.range ↑(algebraMap F E) ∪ S)) ↔
    x ∈ Subfield.closure (Set.range ↑(algebraMap F E') ∪ ↑f '' S)
rw [RingHom.map_field_closure, Set.image_union, ← Set.range_comp, ← RingHom.coe_comp,
  f.comp_algebraMap]
no goals
case h
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
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E'
⊢ x ∈ Subfield.closure (Set.range ↑(algebraMap F E') ∪ ↑↑f '' S) ↔
    x ∈ Subfield.closure (Set.range ↑(algebraMap F E') ∪ ↑f '' S)
rfl