M : Type u_1
N : Type u_2
P : Type ?u.13819
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_3
mc : MonoidHomClass F M N
f : F
S : Submonoid M
y : N
⊢ y ∈ map f S ↔ ∃ x x_1, ↑f x = y
M : Type u_1
N : Type u_2
P : Type ?u.13819
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_3
mc : MonoidHomClass F M N
f : F
S : Submonoid M
y : N
⊢ y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
rw [← bex_def]
no goals
M : Type u_1
N : Type u_2
P : Type ?u.13819
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S✝ : Submonoid M
F : Type u_3
mc : MonoidHomClass F M N
f : F
S : Submonoid M
y : N
⊢ y ∈ map f S ↔ ∃ x x_1, ↑f x = y
exact mem_image_iff_bex