no goals
G : Type u_2
G' : Type ?u.564457
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.564466
inst✝¹ : AddGroup A
N : Type u_1
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑(map f (comap f H)) = ↑(range f ⊓ H)
rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]