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