G : Type u_1
G' : Type ?u.242723
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.242732
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.242759
inst✝ : Group P
f : G →* N
K : Subgroup G
y : N
⊢ (∃ x x_1, ↑f x = y) ↔ ∃ x, x ∈ K ∧ ↑f x = y
G : Type u_1
G' : Type ?u.242723
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.242732
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.242759
inst✝ : Group P
f : G →* N
K : Subgroup G
y : N
⊢ y ∈ map f K ↔ ∃ x, x ∈ K ∧ ↑f x = y
erw [mem_image_iff_bex]
no goals
G : Type u_1
G' : Type ?u.242723
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.242732
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.242759
inst✝ : Group P
f : G →* N
K : Subgroup G
y : N
⊢ (∃ x x_1, ↑f x = y) ↔ ∃ x, x ∈ K ∧ ↑f x = y
simp