no goals
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
f : R ≃+* S
K : Subsemiring R
x : S
⊢ x ∈ map (↑f) K ↔ ↑(RingEquiv.symm f) x ∈ K
convert @Set.mem_image_equiv _ _ (↑K) f.toEquiv x using 1