no goals
G : Type u_1
G' : Type ?u.599712
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.599721
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ f : G →* N
g : N →* G
hl : LeftInverse ↑g ↑f
hr : Function.RightInverse ↑g ↑f
H : Subgroup G
⊢ ↑(map f H) = ↑(comap g H)
rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]