F : Type u_2
inst✝¹ : Field F
S : Set F
K : Type u_1
inst✝ : Field K
f : F →+* K
⊢ IsSubfield (↑f '' Set.univ)
F : Type u_2
inst✝¹ : Field F
S : Set F
K : Type u_1
inst✝ : Field K
f : F →+* K
⊢ IsSubfield (Set.range ↑f)
rw [← Set.image_univ]
no goals
F : Type u_2
inst✝¹ : Field F
S : Set F
K : Type u_1
inst✝ : Field K
f : F →+* K
⊢ IsSubfield (↑f '' Set.univ)
apply Image.isSubfield _ Univ.isSubfield