F : Type u_2
inst✝¹ : Field F
S : Set F
K : Type u_1
inst✝ : Field K
f : F →+* K
s : Set K
hs : IsSubfield s
src✝ : IsSubring (↑f ⁻¹' s) := RingHom.isSubring_preimage f hs.toIsSubring
a : F
ha : ↑f a ∈ s
⊢ (↑f a)⁻¹ ∈ s
F : Type u_2
inst✝¹ : Field F
S : Set F
K : Type u_1
inst✝ : Field K
f : F →+* K
s : Set K
hs : IsSubfield s
src✝ : IsSubring (↑f ⁻¹' s) := RingHom.isSubring_preimage f hs.toIsSubring
a : F
ha : ↑f a ∈ s
⊢ ↑f a⁻¹ ∈ s
rw [map_inv₀]
no goals
F : Type u_2
inst✝¹ : Field F
S : Set F
K : Type u_1
inst✝ : Field K
f : F →+* K
s : Set K
hs : IsSubfield s
src✝ : IsSubring (↑f ⁻¹' s) := RingHom.isSubring_preimage f hs.toIsSubring
a : F
ha : ↑f a ∈ s
⊢ (↑f a)⁻¹ ∈ s
exact hs.inv_mem ha