no goals
G : Type u_1
G' : Type ?u.580217
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.580226
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ f : G →* N
h : Surjective ↑f
K L : Subgroup N
⊢ comap f K = comap f L → K = L
simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]