no goals
G : Type u_1
G' : Type ?u.582453
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.582462
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ f : G →* N
H : Subgroup G
h : ker f ≤ H
⊢ comap f (map f H) = H
rwa [comap_map_eq, sup_eq_left]