no goals
G : Type u_1
G' : Type ?u.588384
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.588393
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ f : G →* N
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ⊔ ker f ≤ K ⊔ ker f
simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true_iff]