G : Type u_1
G' : Type ?u.254283
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.254292
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.254319
inst✝ : Group P
f : G ≃* N
K : Subgroup G
x : N
⊢ ↑f.symm x ∈ ↑K ↔ ↑(MulEquiv.symm f) x ∈ K
G : Type u_1
G' : Type ?u.254283
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.254292
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.254319
inst✝ : Group P
f : G ≃* N
K : Subgroup G
x : N
⊢ x ∈ map (MulEquiv.toMonoidHom f) K ↔ ↑(MulEquiv.symm f) x ∈ K
erw [@Set.mem_image_equiv _ _ (↑K) f.toEquiv x]
no goals
G : Type u_1
G' : Type ?u.254283
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.254292
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.254319
inst✝ : Group P
f : G ≃* N
K : Subgroup G
x : N
⊢ ↑f.symm x ∈ ↑K ↔ ↑(MulEquiv.symm f) x ∈ K
rfl