no goals
G : Type u_1
G' : Type ?u.577797
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.577806
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ f : G →* N
K L : Subgroup N
hf : Surjective ↑f
⊢ comap f K < comap f L ↔ K < L
simp_rw [lt_iff_le_not_le, comap_le_comap_of_surjective hf]